Adding Equations to System F Types, Neelakantan R. Krishnaswami, Nick Benton. Accepted for publication at ESOP 2012.
Adding Equations to System F Types, Neelakantan R. Krishnaswami, Nick Benton. Accepted for publication at ESOP 2012.
Higher-Order Functional Reactive Programming in Bounded Space, Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann. Accepted for publication at POPL 2012.
A Semantic Model for Graphical User Interfaces, Neelakantan R. Krishnaswami, Nick Benton. Appeared in ICFP 2011.
Ultrametric Semantics of Reactive Programs, Neelakantan R. Krishnaswami, Nick Benton. Preprint. Appeared in LICS 2011.
You can download the source code for the implementation of the language in the paper. You need Ocaml 3.11 or higher, and the Lablgtk2 GUI library.
Focusing on Pattern Matching, Neelakantan R. Krishnaswami. Appeared in POPL 2009.
Permission-Based Ownership: Encapsulating State in Higher-Order Typed Languages, Neel Krishnaswami and Jonathan Aldrich. Appeared in PLDI 2005.
The Inverse Method for the Logic of Bunched Implications, Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Steven Magill and Sungwoo Park. Appeared in LPAR 2004. (Copyright Springer-Verlag)
Verifying Event-Driven Programs using Ramified Frame Properties, Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal. Appeared in TLDI 2010.
Design Patterns in Separation Logic, Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse. Appeared in TLDI 2009.
Modular Verification of the Subject-Observer Pattern via Higher-Order Separation Logic, Neelakantan R. Krishnaswami, Lars Birkedal, and Jonathan Aldrich. Unpublished draft, presented at the FTFJP 2007 workshop.
Separation Logic for a Higher-Order Typed Language, Neel Krishnaswami. Unpublished draft, presented at SPACE 2006 workshop.
A Modal Sequent Calculus for Propositional Separation Logic, Neelakantan R. Krishnaswami. Unpublished draft, presented at IMLA 2008 workshop (Intuitionistic Modal Logic and Applications). Note: the sequent calculus in this paper, while satisfying cut-elimination, is NOT sound with respect to the Kripke semantics of separation logic! The proof in the draft is incorrect.
Idealized ML and Its Separation Logic, Neelakantan R. Krishnaswami, Lars Birkedal, Jonathan Aldrich, John C. Reynolds. Submitted for publication to POPL 2007.
Gordon Plotkin, Lambda-definability and Logical Relations, unpublished manuscript, Edinburgh 1973.
This is where, as far as I know, the phrase "logical relation" originates.
Update: Rick Statman tells me that Mike Gordon coined the phrase logical relation, and that he and Gordon Plotkin picked it up from him.