[Hol-info] Call for participation: Workshop on Mechanizing Metatheory

[Benjamin P. <bcp...@ci...>]

             ACM SIGPLAN Workshop on Mechanizing Metatheory

                           25 September, 2010
                          Baltimore, Maryland
                        (Co-located with ICFP'10)

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


SPECIAL 5TH ANNIVERSARY PROGRAM

  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. The goal of the WMM workshops is to bring
  researchers who are (or would like to be) using automated proof assistants
  for programming language metatheory together with developers of proof
  assistants with an interest in supporting research in programming
  languages.

  This WMM is an occasion to look back at five years of intensive effort on
  formalizing programming languages. The centerpiece of the event will be a
  series of invited talks in which major players in the area look both back
  and forward, offering their perspectives on what has been achieved and
  what challenges remain.  A session of contributed talks rounds out the
  day.

INVITED TALKS

  Andrew Appel (Princeton University)
    Modular Foundational Verification of the Software Toolchain

  Steve Zdancewic (University of Pennsylvania)
    Living with Locally Nameless

  Christian Urban (TU Munich)
    Nominal Isabelle: The Last 5 Years and the Next 5 Years

  Karl Crary (Carnegie Mellon University)
    Mechanization of Full-Scale Languages

  Amy Felty (University of Ottawa)
    Reasoning with Higher-Order Abstract Syntax in Hybrid 
    and Related Systems

CONTRIBUTED TALKS

  Yukiyoshi Kameyama (University of Tsukuba), Oleg Kiselyov
  (FNMOC), Chung-chieh Shan (Rutgers University)
    Mechanizing multilevel metatheory with control effects

  James Cheney (University of Edinburgh)
    Mechanized metatheory: ready for prime time?

  Benoit Montagu (INRIA)
    Experience report: Mechanizing Core F-zip using the locally
    nameless approach

  Scott Owens and Peter Sewell (University of Cambridge),
  Stephanie Weirich (University of Pennsylvania), 
  Francesco Zappa Nardelli (INRIA)
    Ott Or Nott


REGISTRATION AND LOCAL ARRANGEMENTS

  * https://regmaster3.com/2010conf/ICFP10/register.php
  * http://www.icfpconference.org/icfp2010/local.html


WORKSHOP ORGANIZATION

  PROGRAM COMMITTEE
    Elsa Gunter, University of Illinois
    Tobias Nipkow, TU Munich
    Frank Pfenning, Carnegie Mellon
    Benjamin Pierce, University of Pennsylvania (chair)

  STEERING COMMITTEE
    Karl Crary, Carnegie Mellon University
    Michael Norrish, National ICT Australia
    Stephanie Weirich, University of Pennsylvania
    Christian Urban, TU Munich