MCK: Model Checking the Logic of Knowledge. - Peter Gammie; Ron van der Meyden (CAV, 2004)

Model Checking Knowledge and Linear Time: PSPACE Cases. - Kai Engelhardt; Peter Gammie; Ron van der Meyden (LFCS, 2007)

Some classical results in Social Choice Theory. - Peter Gammie (Arch. Formal Proofs, 2008)

The Worker/Wrapper Transformation. - Peter Gammie (Arch. Formal Proofs, 2009)

Peter Van Roy and Seif Haridi. Concepts, Techniques, and Models of Computer Programming. The MIT Press, 2004. ISBN: 0262220695 Price $70. 930pp. - Peter Gammie (J. Funct. Program., 2009)

Provable Security: How Feasible Is It? - Gerwin Klein; Toby C. Murray; Peter Gammie; Thomas Sewell; Simon Winwood (HotOS, 2011)

Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments. - Peter Gammie (ITP, 2011)

seL4 Enforces Integrity. - Thomas Sewell; Simon Winwood; Peter Gammie; Toby C. Murray; June Andronick; Gerwin Klein (ITP, 2011)

Knowledge-based programs. - Peter Gammie (Arch. Formal Proofs, 2011)

Review: Lambda-Calculus and Combinators: An Introduction, Second Edition by J. R. Hindley and J. P. Seldin. - Peter Gammie (J. Funct. Program., 2011)

Short note: Strict unwraps make worker/wrapper fusion totally correct. - Peter Gammie (J. Funct. Program., 2011)

Noninterference for Operating System Kernels. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Gerwin Klein (CPP, 2012)

Logical Relations for PCF. - Peter Gammie (Arch. Formal Proofs, 2012)

seL4: From General Purpose to a Proof of Information Flow Enforcement. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Timothy Bourke; Sean Seefried; Corey Lewis; Xin Gao; Gerwin Klein (IEEE Symposium on Security and Privacy, 2013)

Synchronous digital circuits as functional programs. - Peter Gammie (ACM Comput. Surv., 2013)

Concurrent IMP. - Peter Gammie (Arch. Formal Proofs, 2015)

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO. - Peter Gammie; Tony Hosking; Kai Engelhardt (Arch. Formal Proofs, 2015)

The Stern-Brocot Tree. - Peter Gammie; Andreas Lochbihler (Arch. Formal Proofs, 2015)

Stable Matching. - Peter Gammie (Arch. Formal Proofs, 2016)

The Kuratowski Closure-Complement Theorem. - Peter Gammie; Gianpaolo Gioiosa (Arch. Formal Proofs, 2017)

Putting the 'K' into Bird's derivation of Knuth-Morris-Pratt string matching. - Peter Gammie (Arch. Formal Proofs, 2020)

ConcurrentHOL. - Peter Gammie (Arch. Formal Proofs, 2024)