Towards Formalizing Categorical Models of Type Theory in Type Theory. - Alexandre Buisse; Peter Dybjer (LFMTP@CADE, 2007)

The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. - Alexandre Buisse; Peter Dybjer (MFPS, 2008)

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

Step-Indexed Kripke Model of Separation Logic for Storable Locks. - Alexandre Buisse; Lars Birkedal; Kristian Støvring (MFPS, 2011)