Neel Krishnaswami
where else to find them
what they talk about
all 6 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 20 in the filters
who talks about the same things
- Kayvan Memarian6 talks
- Christopher Pulte4 talks
- Peter Sewell14 talks
- Ranjit Jhala19 talks
- Amal Ahmed25 talks
- Vikraman Choudhury10 talks
| title | conference | date |
|---|---|---|
| Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…) | PLDI 2026 | 2026-06-15 |
Integrates CN separation logic into runtime checks, unit and SMT-based random generator testing, and final machine-checked proofs, all on the real-world PKVM… | ||
| Sound and Complete Refinement for SSA with Substructural Effects | HOPE 2025 | 2025-10-12 |
A denotational model for SSA is given and a syntactic refinement relation is defined that is proven sound and complete against postset-enriched categories, so… | ||
| Semantic Analysis of Normalisation for Directional Logic Programming | WITS 2025 | 2025-01-25 |
Claims a formal bridge: bidirectional type checking becomes directional logic programs whose evaluation is normalisation as cut reductions in classical linear… | ||
| Fulminate: Testing CN Separation-Logic Specifications in C | POPL 2025 | 2025-01-19 |
Fulminate translates CN separation-logic annotations into executable C checks that enforce ownership ghost state and explicit ownership transfer at runtime… | ||
| How to Give a Talk | PLMW @ POPL 2024 | 2024-01-17 |
Science is collective so talks sit between one‑on‑one conversations and papers and must manage attention by motivating a problem, giving a roadmap, and… | ||
| Focusing on Refinement Typing (TOPLAS) | POPL 2024 | 2024-01-14 |
A logically principled system that combines value-determined indices, focalized call-by-push-value, bidirectional typing and polarized subtyping generates SMT… | ||
| Explicit Refinement Types | ICFP 2023 | 2023-09-04 |
System called λert implements refinement types that require explicit, checkable proofs instead of SMT solving, supporting quantifiers and induction; key claim… | ||
| CN: Verifying Systems C Code with Separation-Logic Refinement Types | POPL 2023 | 2023-01-15 |
CN is a separation-logic refinement type system for ISO C that uses a Cerberus translation to a core language, implements resource types as first-class… | ||
| Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic | POPL 2022 | 2022-01-16 |
Claims a source to source transformation that produces dual numbers then generalizes to multi dual numbers and a compact symbolic delta representation… | ||
| Recovering Purity with Comonads and Capabilities | ICFP 2020 | 2020-08-23 |
A call-by-value impure lambda calculus is extended with a comonadic safety modality that tags variables as safe or impure and a box comonad that internalizes… | ||
| nothing matches | ||