"Focusing on Pattern Matching", Neelakantan R. Krishnaswami, accepted for publication at POPL 2009.
"Design Patterns in Separation Logic", Neelakantan R. Krishnaswami, Jonathan Aldrich, Lars Birkedal, Kasper Svendsen, Alexandre Buisse. Accepted for publication at TLDI 2009.
"Permission-Based Ownership: Encapsulating State in Higher-Order Typed Languages", Neel Krishnaswami and Jonathan Aldrich. Published 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.
Notes on Regular Tree Automata
Super-high level notes on ownership
Medium-high level notes on ownership
Slides for PLDI Ownership Talk