Peter Gammie

22 papers A* 3A 1B 3Misc 1Journal 14
YearRankTypeTitle / Venue / Authors
2024 J jnl
ConcurrentHOL.
Arch. Formal Proofs
Peter Gammie
2020 J jnl
Putting the 'K' into Bird's derivation of Knuth-Morris-Pratt string matching.
Arch. Formal Proofs
Peter Gammie
2017 J jnl
The Kuratowski Closure-Complement Theorem.
Arch. Formal Proofs
Peter Gammie, Gianpaolo Gioiosa
2016 J jnl
Stable Matching.
Arch. Formal Proofs
Peter Gammie
2015 J jnl
Concurrent IMP.
Arch. Formal Proofs
Peter Gammie
2015 J jnl
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO.
Arch. Formal Proofs
Peter Gammie, Tony Hosking, Kai Engelhardt
2015 A* conf
Relaxing safely: verified on-the-fly garbage collection for x86-TSO.
PLDI
Peter Gammie, Antony L. Hosking, Kai Engelhardt
2015 J jnl
The Stern-Brocot Tree.
Arch. Formal Proofs
Peter Gammie, Andreas Lochbihler
2013 J jnl
Synchronous digital circuits as functional programs.
ACM Comput. Surv.
Peter Gammie
2013 A* conf
seL4: From General Purpose to a Proof of Information Flow Enforcement.
IEEE Symposium on Security and Privacy
Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein
2012 J jnl
Logical Relations for PCF.
Arch. Formal Proofs
Peter Gammie
2012 B conf
Noninterference for Operating System Kernels.
CPP
Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
2011 J jnl
Knowledge-based programs.
Arch. Formal Proofs
Peter Gammie
2011 A conf
Provable Security: How Feasible Is It?
HotOS
Gerwin Klein, Toby C. Murray, Peter Gammie, Thomas Sewell, Simon Winwood
2011 J jnl
Short note: Strict unwraps make worker/wrapper fusion totally correct.
J. Funct. Program.
Peter Gammie
2011 B conf
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments.
ITP
Peter Gammie
2011 B conf
seL4 Enforces Integrity.
ITP
Thomas Sewell, Simon Winwood, Peter Gammie, Toby C. Murray, June Andronick, Gerwin Klein
2009 J jnl
Peter Van Roy and Seif Haridi.
J. Funct. Program.
Peter Gammie
2009 J jnl
The Worker/Wrapper Transformation.
Arch. Formal Proofs
Peter Gammie
2008 J jnl
Some classical results in Social Choice Theory.
Arch. Formal Proofs
Peter Gammie
2007 Misc conf
Model Checking Knowledge and Linear Time: PSPACE Cases.
LFCS
Kai Engelhardt, Peter Gammie, Ron van der Meyden
2004 A* conf
MCK: Model Checking the Logic of Knowledge.
CAV
Peter Gammie, Ron van der Meyden