[TYPES/announce] Workshop on Mechanizing Metatheory Program

[Stephanie Weirich]

-------------------------------------------------------------------
                    Call for Participation

          1st Informal ACM SIGPLAN Workshop on
                   Mechanizing Metatheory

                 September 21, 2006
                       Portland, OR, USA

                Immediately following ICFP 2006

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


Dear all,

    I am pleased to announce the program for the first ever workshop on
    mechanizing programming language metatheory. I look forward to seeing
    you in Portland!

   Note that the early registration deadline is coming soon---August
   18th! That is also the cutoff date for the hotel. See the ICFP
   web page (http://icfp06.cs.uchicago.edu/) for more logistical
   information.
    
    See you soon,

    Stephanie

----------------------- Program ----------------------------------

Thursday, September 21, 2006

Session I:9-10, chair Michael Norrish (Canberra Research Lab, National 
ICT Australia)

  On the Formalization of Logical Relation Arguments
  Jeffrey Sarnat (Yale University) and Carsten Schuermann (IT University
  of Copenhagen)

  Explicit Contexts in LF
  Karl Crary (Carnegie Mellon University)

Session II:10:30-12, chair Karl Crary (Carnegie Mellon University)

  A Comparison between Concrete Representations for Bindings
  Arthur Chargueraud (ENS, Paris)

  Towards a Coq Library for Programming Languages Meta-Theory with 
Concrete Names
  Aaron Stump (Washington University in St. Louis)

  Mechanized Reasoning for Binding Constructs in Types Assembly Language 
Using Coq
  Nadeem Hamid (Berry College)

Session III: 14-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)

  Proof Weaving
  Anne Mulhern (University of Wisconsin-Madison)

  Mechanized Metatheory Model-Checking
  James Cheney (University of Edinburgh)

Session IV:16-17, chair Stephanie Weirich (University of Pennsylvania)

  Mechanizing the Metatheory of an Elaborative Semantics for Standard ML
  Daniel Lee, Karl Crary, Robert Harper (Carnegie Mellon University)

  Mechanized Metatheory for User-Defined Type Extensions
  Daniel Marino, Brian Chin, Todd Millstein (University of California,
  Los Angeles), Gang Tan (Boston College), Rob Simmons, and David
  Walker (Princeton University)