1st Informal ACM SIGPLAN
Workshop on Mechanizing Metatheory

Portland, Oregon, USA

Sponsored by ACM SIGPLAN

Co-located with ICFP'06.

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

Thursday, September 21, 2006

• Session I: 9:00-10:00, chair Steve Zdancewic (University of Pennsylvania)
  
  
• On the Formalization of Logical Relation Arguments
  Jeffrey Sarnat (Yale University) and Carsten Schürmann (IT University of Copenhagen)
  [slides][source code: lr-st.tgz, lr-f.tgz]
  
  
• Explicit Contexts in LF
  Karl Crary (Carnegie Mellon University)
  [slides]
  
  
• Session II:10:30-12:00, chair Karl Crary (Carnegie Mellon University)
  
  
• A Comparison between Concrete Representations for Bindings
  Arthur Charguéraud (ENS Lyon / ENS Cachan)
  [slides][source code: stlc.v, fsub.v]
  
  
• Towards a Coq Library for Programming Languages Meta-Theory with Concrete Names
  Aaron Stump (Washington University in St. Louis)
  [slides]
  
  
• Mechanized Reasoning for Binding Constructs in Types Assembly Language Using Coq
  Nadeem Hamid (Berry College)
  [slides][source code]
  
  
• Session III: 14:00-15:30, chair Peter Sewell (Cambridge University)
  
  
• Machine Obstructed Proof: How many months can it take to verify 30 assembly instructions?
  Nick Benton (Microsoft Research)
  [slides]
  
  
• Proof Weaving
  Anne Mulhern (University of Wisconsin-Madison)
  
  
• Mechanized Metatheory Model-Checking
  James Cheney (University of Edinburgh)
  [slides][full paper]
  
  
• Session IV:16:00-17:00, chair Stephanie Weirich (University of Pennsylvania)
  
  
• Mechanizing the Metatheory of Standard ML
  Daniel Lee, Karl Crary, Robert Harper (Carnegie Mellon University)
  [slides][source code]
  
  
• Mechanized Metatheory for User-Defined Type Extensions
  Daniel Marino, Brian Chin, Todd Millstein (University of California, Los Angeles), Gang Tan (Boston College), Robert J. Simmons, and David Walker (Princeton University)
  [slides]