The Inverse Method for the Logic of Bunched Implications. - Kevin Donnelly; Tyler Gibson; Neel Krishnaswami; Stephen Magill; Sungwoo Park (LPAR, 2004)

Permission-based ownership: encapsulating state in higher-order typed languages. - Neelakantan R. Krishnaswami; Jonathan Aldrich (PLDI, 2005)

Reasoning about iterators with separation logic. - Neelakantan R. Krishnaswami (SAVCBS@FSE, 2006)

Focusing on pattern matching. - Neelakantan R. Krishnaswami (POPL, 2009)

Design patterns in separation logic. - Neelakantan R. Krishnaswami; Jonathan Aldrich; Lars Birkedal; Kasper Svendsen; Alexandre Buisse (TLDI, 2009)

Verifying event-driven programs using ramified frame properties. - Neel Krishnaswami; Lars Birkedal; Jonathan Aldrich (TLDI, 2010)

A semantic model for graphical user interfaces. - Neelakantan R. Krishnaswami; Nick Benton (ICFP, 2011)

Ultrametric Semantics of Reactive Programs. - Neelakantan R. Krishnaswami; Nick Benton (LICS, 2011)

Adding Equations to System F Types. - Neelakantan R. Krishnaswami; Nick Benton (ESOP, 2012)

Superficially substructural types. - Neelakantan R. Krishnaswami; Aaron Turon; Derek Dreyer; Deepak Garg 001 (ICFP, 2012)

Higher-order functional reactive programming in bounded space. - Neelakantan R. Krishnaswami; Nick Benton; Jan Hoffmann 002 (POPL, 2012)

Semantics for graphical user interfaces. - Neelakantan R. Krishnaswami (TLDI, 2012)

Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. - Neelakantan R. Krishnaswami (2012)

Internalizing Relational Parametricity in the Extensional Calculus of Constructions. - Neelakantan R. Krishnaswami; Derek Dreyer (CSL, 2013)

Complete and easy bidirectional typechecking for higher-rank polymorphism. - Jana Dunfield; Neelakantan R. Krishnaswami (ICFP, 2013)

Higher-order functional reactive programming without spacetime leaks. - Neelakantan R. Krishnaswami (ICFP, 2013)

Freeze after writing: quasi-deterministic parallel programming with LVars. - Lindsey Kuper; Aaron Turon; Neelakantan R. Krishnaswami; Ryan R. Newton (POPL, 2014)

Integrating Linear and Dependent Types. - Neelakantan R. Krishnaswami; Cécilia Pradic; Nick Benton (POPL, 2015)

Mtac: A monad for typed tactic programming in Coq. - Beta Ziliani; Derek Dreyer; Neelakantan R. Krishnaswami; Aleksandar Nanevski; Viktor Vafeiadis (J. Funct. Program., 2015)

Datafun: a functional Datalog. - Michael Arntzenius; Neelakantan R. Krishnaswami (ICFP, 2016)

NumLin: Linear Types for Linear Algebra. - Dhruv C. Makwana; Neelakantan R. Krishnaswami (ECOOP, 2019)

A Program Logic for First-Order Encapsulated WebAssembly. - Conrad Watt; Petar Maksimovic 001; Neelakantan R. Krishnaswami; Philippa Gardner (ECOOP, 2019)

Representing music with prefix trees. - Yan Han; Nada Amin; Neel Krishnaswami (FARM@ICFP, 2019)

A typed, algebraic approach to parsing. - Neelakantan R. Krishnaswami; Jeremy Yallop (PLDI, 2019)

NumLin: Linear Types for Linear Algebra (Artifact). - Dhruv C. Makwana; Neelakantan R. Krishnaswami (Dagstuhl Artifacts Ser., 2019)

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. - Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Alastair Reid 001; Kathryn E. Gray; Robert M. Norton; Prashanth Mundkur; Mark Wassell; Jon French; Christopher Pulte; Shaked Flur; Ian Stark; et al. (Proc. ACM Program. Lang., 2019)

Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. - Jana Dunfield; Neelakantan R. Krishnaswami (Proc. ACM Program. Lang., 2019)

Adjoint Reactive GUI. - Christian Uldal Graulund; Dmitrij Szamozvancev; Neel Krishnaswami (CoRR, 2020)

Seminaïve evaluation for a higher-order functional language. - Michael Arntzenius; Neel Krishnaswami (Proc. ACM Program. Lang., 2020)

Recovering purity with comonads and capabilities. - Vikraman Choudhury; Neel Krishnaswami (Proc. ACM Program. Lang., 2020)

Adjoint Reactive GUI Programming. - Christian Uldal Graulund; Dmitrij Szamozvancev; Neel Krishnaswami (FoSSaCS, 2021)

Transfinite step-indexing for termination. - Simon Spies; Neel Krishnaswami; Derek Dreyer (Proc. ACM Program. Lang., 2021)

Implicit Polarized F: local type inference for impredicativity. - Henry Mercer; Cameron Ramsay; Neel Krishnaswami (CoRR, 2022)

Focusing on Liquid Refinement Typing. - Dimitrios J. Economou; Neel Krishnaswami; Jana Dunfield (CoRR, 2022)

Bidirectional Typing. - Jana Dunfield; Neel Krishnaswami (ACM Comput. Surv., 2022)

Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation. - Faustyna Krawiec; Simon Peyton Jones; Neel Krishnaswami; Tom Ellis; Richard A. Eisenberg; Andrew W. Fitzgibbon (Proc. ACM Program. Lang., 2022)

flap: A Deterministic Parser with Fused Lexing. - Jeremy Yallop; Ningning Xie; Neel Krishnaswami (Proc. ACM Program. Lang., 2023)

CN: Verifying Systems C Code with Separation-Logic Refinement Types. - Christopher Pulte; Dhruv C. Makwana; Thomas Sewell; Kayvan Memarian; Peter Sewell; Neel Krishnaswami (Proc. ACM Program. Lang., 2023)

Explicit Refinement Types. - Jad Elkhaleq Ghalayini; Neel Krishnaswami (Proc. ACM Program. Lang., 2023)

Focusing on Refinement Typing. - Dimitrios J. Economou; Neel Krishnaswami; Jana Dunfield (ACM Trans. Program. Lang. Syst., 2023)

Implementing a Type Theory with Observational Equality, Using Normalisation by Evaluation. - Matthew Sirman; Meven Lennon-Bertrand; Neel Krishnaswami (TYPES, 2024)

The Denotational Semantics of SSA. - Jad Elkhaleq Ghalayini; Neel Krishnaswami (CoRR, 2024)

Fulminate: Testing CN Separation-Logic Specifications in C. - Rini Banerjee; Kayvan Memarian; Dhruv C. Makwana; Christopher Pulte; Neel Krishnaswami; Peter Sewell (Proc. ACM Program. Lang., 2025)