peteg's webspace - papers

You can find BibTeX entries and so forth at DBLP. My thesis work may also be of interest.

Papers

• Relaxing safely: verified on-the-fly garbage collection for x86-TSO, ACM PLDI (2015) (with Tony Hosking and Kai Engelhardt).
• Synchronous digital circuits as functional programs, ACM Computing Surveys (2013).
• seL4: from General Purpose to a Proof of Information Flow Enforcement, IEEE Symposium on Security and Privacy (2013) (with Toby Murray, Daniel Matichuk, Matthew Brassil, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein).
• Noninterference for Operating System Kernels, The Second International Conference on Certified Programs and Proofs (2012) (with Toby Murray, Daniel Matichuk, Matthew Brassil and Gerwin Klein).
• Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments, Interactive Theorem Proving (2011).
• seL4 Enforces Integrity, Interactive Theorem Proving (2011) (with Thomas Sewell, Simon Winwood, Toby Murray, June Andronick and Gerwin Klein).
• Provable Security: How Feasible Is It?, USENIX HOTOS XIII (2011) (with Gerwin Klein, Toby Murray, Thomas Sewell, and Simon Winwood).
• Short note: Strict unwraps make worker/wrapper fusion totally correct, Journal of Functional Programming 21(2): 209-213 (2011).
• Model Checking Knowledge and Linear Time: PSPACE Cases, LFCS (2007) (with Kai Engelhardt and Ron van der Meyden).
• MCK: Model Checking the Logic of Knowledge, CAV (2004) (with Ron van der Meyden).

Isabelle Theories

The following are available at the Archive of Formal Proofs:

• Stable Matching, about matching-with-contracts in the stable marriage tradition.
• Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO. Companion to the PLDI 2015 paper.
• Concurrent IMP. Companion to the PLDI 2015 paper.
• The Stern-Brocot Tree with Andreas Lochbihler.
• Logical Relations for PCF. A mechanisation of several classic results about Gordon Plotkin's PCF language using Andy Pitts's domain-theoretic machinery.
• Knowledge-based programs. Companion to the ITP 2011 paper.
• The Worker/Wrapper Transformation. Companion to the JFP 2011 paper.
• Some classical results in social choice theory. A mechanisation of some of Sen's classic Collective Choice and Social Welfare, particularly Arrow's Theorem.

Book reviews

• J. R. Hindley and J. P. Seldin. Lambda-Calculus and Combinators: An Introduction, Second Edition. Journal of Functional Programming 21(1): 115-117 (2011).
• Peter Van Roy and Seif Haridi. Concepts, Techniques, and Models of Computer Programming. The MIT Press, 2004., Journal of Functional Programming 19(2): 254-256 (2009).