2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory

Freiburg, Germany

Sponsored by ACM SIGPLAN

Co-located with ICFP’07.

http://www.cis.upenn.edu/~sweirich/wmm/

Thursday, 4 October 2007

Session I: 9:00–10:00

• A Mechanized Framework for Aspects in Isabelle/HOL. F. Kammüller and H. Sudhof. [Abstract][Slides]
• Specifying real-world binding structures. Susmit Sarkar, Peter Sewell and Francesco Zappa Nardelli. [Abstract][Slides]

Session II: 10:30–12:00

• Verifying type soundness in HOL for OCaml: the core language. Scott Owens and Gilles Peskine. [Abstract][Slides]
• Mechanised Proofs of Type Safety for a Family of Lambda Calculi with References. Michalis A. Papakyriakou and Nikolaus S. Papaspyrou. [Abstract][Slides][Handout][Code]
• To arrive where we started: experience of mechanizing binding. Tom Ridge. [Abstract][Slides]

Session III: 14:00–15:30

• Mechanizing a Decision Procedure for Coproduct Equality Arbob Ahmad, Daniel R. Licata and Robert Harper. [Abstract][Slides]
• A Framework for Language-Based Cryptographic Proofs. Gilles Barthe, Benjamin Grégoire, Romain Janvier and Santiago Zanella Béguelin. [Abstract][Slides]
• Generic Programming and Proving for Programming Language Metatheory. Adam Chlipala. [Abstract][Slides][Author's page]
  

Session IV: 16:00–17:00

• Applications of Metatheory: Verification of Compiler Optimisations. Richard Warburton and Sara Kalvala. [Abstract][Slides]
• Locally Nameless Representation in Nominal Isabelle. Christian Urban and Robert Pollack. [Abstract][Slides]