5th ACM SIGPLAN Workshop on Mechanizing Metatheory

25 September, 2010
Baltimore, Maryland

Co-located with ICFP’10

Sponsored by ACM SIGPLAN

Special 5th Anniversary Program

[Preliminary schedule: still subject to change!]

8:00 - 8:45      Continental breakfast
9:00 - 10:00 Andrew Appel (Princeton University)
Modular Foundational Verification of the Software Toolchain (Invited Talk)
10:00 - 10:30 Break
10:30 - 11:30 Christian Urban (TU Munich)
Nominal Isabelle or, How I learned to stop worrying and love the Variable Convention (Invited Talk)
11:30 - 11:50 Yukiyoshi Kameyama (University of Tsukuba), Oleg Kiselyov (FNMOC), Chung-chieh Shan (Rutgers University)
Mechanizing multilevel metatheory with control effects
11:50 - 12:10 James Cheney (University of Edinburgh)
Mechanized metatheory: ready for prime time?
12:10 - 12:30 Benoit Montagu (INRIA)
Experience report: Mechanizing Core F-zip using the locally nameless approach
12:30 - 2:00 Lunch
2:00 - 3:00 Karl Crary (Carnegie Mellon University)
Mechanization of Full-Scale Languages (Invited Talk)
3:00 - 3:30 Break
3:30 - 4:30 Amy Felty (University of Ottawa)
Reasoning with Higher-Order Abstract Syntax in Hybrid and Related Systems (Invited Talk)
4:30 - 5:00 Break
5:00 - 5:30 Steve Zdancewic (University of Pennsylvania)
Living with Locally Nameless (Invited Talk)
5:30 - 6:00 Scott Owens and Peter Sewell (University of Cambridge), Stephanie Weirich (University of Pennsylvania), Francesco Zappa Nardelli (INRIA)
Ott Or Nott


Christian Urban
Nominal Isabelle or, How I learned to stop worrying and love the Variable Convention

The aim of Nominal Isabelle is to provide a convenient reasoning infrastructure for languages involving named binders (as opposed to de Bruijn indices). In the talk I will explain how we deal with the informal variable convention in a formal setting and how this convention can lead to faulty proofs, if not appropriately restricted. I will also describe our current work about general binding structures, which are often used in programming language research.