Deduction for Functional Programmers. - James J. Leifer; Bernard Sufrin (J. Funct. Program., 1996)

Deriving Bisimulation Congruences for Reactive Systems. - James J. Leifer; Robin Milner (CONCUR, 2000)

Operational congruences for reactive systems - James J. Leifer (2001)

Shallow Linear Action Graphs and their Embeddings. - James J. Leifer; Robin Milner (Formal Aspects Comput., 2002)

Global abstraction-safe marshalling with hash types. - James J. Leifer; Gilles Peskine; Peter Sewell; Keith Wansbrough (ICFP, 2003)

Abstraction preservation and subtyping in distributed languages. - Pierre-Malo Deniélou; James J. Leifer (ICFP, 2006)

Transition systems, link graphs and Petri nets. - James J. Leifer; Robin Milner (Math. Struct. Comput. Sci., 2006)

Secure Implementations for Typed Session Abstractions. - Ricardo Corin; Pierre-Malo Deniélou; Cédric Fournet; Karthikeyan Bhargavan; James J. Leifer (CSF, 2007)

Acute: High-level programming language design for distributed computation. - Peter Sewell; James J. Leifer; Keith Wansbrough; Francesco Zappa Nardelli; Mair Allen-Williams; Pierre Habouzit; Viktor Vafeiadis (J. Funct. Program., 2007)

A secure compiler for session abstractions. - Ricardo Corin; Pierre-Malo Deniélou; Cédric Fournet; Karthikeyan Bhargavan; James J. Leifer (J. Comput. Secur., 2008)

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. - Karthikeyan Bhargavan; Ricardo Corin; Pierre-Malo Deniélou; Cédric Fournet; James J. Leifer (CSF, 2009)