"Verifying Event-Driven Programs using Ramified Frame Properties", Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal. Accepted at TLDI 2010.
"Focusing on Pattern Matching", Neelakantan R. Krishnaswami, Appeared in POPL 2009.
"Design Patterns in Separation Logic", Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse. Appeared in TLDI 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)
"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.
Notes on Regular Tree Automata
Super-high level notes on ownership
Medium-high level notes on ownership
Slides for PLDI Ownership Talk