peteg's webspace - papers

You can find BibTeX entries and so forth at DBLP.

Papers

• 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:

• 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

• Lambda-Calculus and Combinators: An Introduction, Second Edition by J. R. Hindley and J. P. Seldin., 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).