3rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory

Victoria, British Columbia, Canada

Sponsored by ACM SIGPLAN

Co-located with ICFP’08.


20 September 2008

Session I: 9:00-10:30
Formalizing an Extensional Semantics for Units of Measure
Andrew Kennedy
Microsoft Research Cambridge

Proving correctness of a dynamic atomicity analysis in Coq
Caitlin Sadowski, Jaeheon Yi, Kenneth Knowles, and Cormac Flanagan
University of California at Santa Cruz

Mechanizing the Metatheory of a Language With Linear Resources and Context Effects
Daniel K. Lee [1], Derek Dreyer [2], and Andreas Rossberg [2]
[1] Carnegie Mellon University
[2] Max Planck Institute for Software Systems

10:30-11:00  Break

Session II:  11:00-12:00
Case Study: Subject Reduction for Mini-ML with References, in Isabelle/HOL + Hybrid
Alan J. Martin
University of Ottawa

Mechanizing Methatheory with Nested Datatypes
Andre Hirschowitz [1] and Marco Maggesi [2]
[1] University of Nice (UNS) and CNRS
[2] University di Firenze

12:00-14:00  Lunch

Session III: 14:00-15:00
Shallow embedding of a logic in Coq
Jerome Vouillon
Universite Paris Diderot - Paris 7, CNRS

Names via Substructural and Dependent Types
Jason Reed
Carnegie Mellon University

15:00-15:30  Break

Session IV: 15:30-17:00
SASyLF: An Educational Proof Assistant for Language Theory
Jonathan Aldrich [1], Robert J. Simmons [1], and Key Shin [2]
[1] Carnegie Mellon University
[2] Microsoft Corporation

Building Verified Language Tools in Operational Type Theory
Aaron Stump
The University of Iowa

5-minute talks