[TYPES/announce] WMM'08 call for participation

[Karl Crary]

Apologies for the cross-posting.

-------------------------



                        CALL FOR PARTICIPATION

                  3rd Informal ACM SIGPLAN Workshop
                      on Mechanizing Metatheory

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

                      Victoria, British Columbia
                          September 20, 2008

                      Co-located with ICFP 2008.


Researchers in programming languages have long felt the need for tools
to help formalize and check their work. With advances in language
technology demanding deep understanding of ever larger and more
complex languages, this need has become urgent. There are a number of
automated proof assistants being developed within the theorem proving
community that seem ready or nearly ready to be applied in this domain
-- yet, despite numerous individual efforts in this direction, the use
of proof assistants in programming language research is still not
commonplace: the available tools are confusingly diverse, difficult to
learn, inadequately documented, and lacking in specific library
facilities required for work in programming languages.

The goal of this workshop is to bring together researchers who have
experience using automated proof assistants for programming language
metatheory, and those who are interested in using tool support for
formalizing their work. One starting point for discussion will be the
obstacles that hinder mechanisation (whether they be pragmatic or
technical), and what users and developers can do to overcome them.


The workshop will conclude with a session of five-minute talks.
Proposals for five-minute talks will be accepted the morning of the
workshop.  Five-minute talks need not be polished, and discussions of
works in progress are encouraged.


Program

Welcome: 8:50-9:00


Session 1: 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


Coffee Break: 10:30-11:00


Session 2: 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] Universita di Firenze


Lunch: 12:00-14:00  


Session 3: 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


Coffee Break: 15:00-15:30


Session 4: 15:30-16:30

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


Five-minute talks: 16:30-17:00