An expressive language of signatures. - Norman Ramsey; Kathleen Fisher; Paul Govereau (ICFP, 2005)

Ynot: dependent types for imperative programs. - Aleksandar Nanevski; Greg Morrisett; Avraham Shinnar; Paul Govereau; Lars Birkedal (ICFP, 2008)

Towards type-theoretic semantics for transactional concurrency. - Aleksandar Nanevski; Paul Govereau; Greg Morrisett (TLDI, 2009)

Evaluating value-graph translation validation for LLVM. - Jean-Baptiste Tristan; Paul Govereau; Greg Morrisett (PLDI, 2011)