From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.6 required=5.0 tests=NO_REAL_NAME autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 40765BBAF for ; Wed, 25 Mar 2009 19:31:39 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am0CAEMVykmBu2+K/2dsb2JhbACVBb5TgjaBPwaHHA X-IronPort-AV: E=Sophos;i="4.38,420,1233529200"; d="scan'208";a="24975722" Received: from math05.mathematik.uni-muenchen.de ([129.187.111.138]) by mail3-smtp-sop.national.inria.fr with ESMTP; 25 Mar 2009 19:31:38 +0100 Received: from math07.mathematik.uni-muenchen.de (math07.mathematik.uni-muenchen.de [129.187.111.132]) by math05.mathematik.uni-muenchen.de (Postfix) with ESMTP id C94CE502185; Wed, 25 Mar 2009 19:31:37 +0100 (CET) Received: by math07.mathematik.uni-muenchen.de (Postfix, from userid 33) id C1D914010FD1; Wed, 25 Mar 2009 19:31:37 +0100 (CET) Received: from 79-67-131-58.dynamic.dsl.as9105.com (79-67-131-58.dynamic.dsl.as9105.com [79.67.131.58]) by webmail.mathematik.uni-muenchen.de (Horde MIME library) with HTTP; Wed, 25 Mar 2009 19:31:37 +0100 Message-ID: <20090325193137.ll7j3wnascw00ok8@webmail.mathematik.uni-muenchen.de> Date: Wed, 25 Mar 2009 19:31:37 +0100 From: urban@math.lmu.de To: types-announce@lists.seas.upenn.edu, poplmark@lists.seas.upenn.edu, haskell@haskell.org, caml-list@inria.fr, smlnj-dev-list@lists.sourceforge.net, MLton-user@mlton.org, plt-scheme@list.cs.brown.edu Subject: WMM'09 call for papers MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; DelSp="Yes"; format="flowed" Content-Disposition: inline Content-Transfer-Encoding: quoted-printable User-Agent: Internet Messaging Program (IMP) H3 (4.1.3) X-Spam: no; 0.00; sigplan:01 co-located:01 formalize:01 formalizing:01 sigplan:01 formalized:01 danvy:01 crary:01 weirich:01 freiburg:01 2009:98 2009:98 upenn:01 pottier:01 printable:01 Call for Papers 4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory Edinburgh, Scotland Co-located with ICFP'09. http://www.cis.upenn.edu/~sweirich/wmm/ Important Dates * Submission deadline: 19 June 2009 * Author Notification: 24 July 2009 * Workshop: 4 September 2009 Workshop Description 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 mechanization (whether they be pragmatic or technical), and what users and developers can do to overcome them. Format The workshop will consist of presentations by the participants, selected from submitted abstracts. It will focus on providing a fruitful environment for interaction and presentation of ongoing work. Participants are invited to submit working notes, source files, and abstracts for distribution to the attendees, but as the workshop has no formal proceedings, contributions may still be submitted for publication elsewhere. (See the SIGPLAN republication policy for more details.) Scope The scope of the workshop includes, but is not limited to: * Tool demonstrations: proof assistants, logical frameworks, visualizers, etc. * Libraries for programming language metatheory. * Formalization techniques, especially with respect to binding issues. * Analysis and comparison of solutions to the POPLmark challenge. * Examples of formalized programming language metatheory. * Proposals for new challenge problems that benchmark programming language work. Submission Guidelines Email submissions to urbanc AT in.tum.de. Submissions should be no longer than two pages in PDF and printable on A4 sized paper. Persons for whom this poses a hardship should contact the program chair. Conference Organization Program Committee * Nick Benton, Microsoft Research Cambridge * Olivier Danvy, University of Aarhus * Daniel Licata, Carnegie Mellon University * Francois Pottier, INRIA Paris-Rocquencourt * Christian Urban, TU Munich (chair) Workshop Organizers * Karl Crary, Carnegie Mellon University * Michael Norrish, National ICT Australia * Stephanie Weirich, University of Pennsylvania Previous Workshops * Victoria, 2008 * Freiburg, 2007 * Portland, 2006 ---------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program.