[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
ACM SIGPLAN Workshop on Mechanizing Metatheory 25 September, 2010 Baltimore, Maryland (Co-located with ICFP'10) http://www.cis.upenn.edu/~bcpierce/wmm/ Submission deadline: 21 July, 2010 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. There will also be a session of short contributed presentations by workshop participants, selected from submitted abstracts. Invited Speakers * Andrew Appel, Princeton University * Karl Crary, Carnegie Mellon University * Amy Felty, University of Ottawa * Christian Urban, TU Munich * Steve Zdancewic, University of Pennsylvania CALL FOR ABSTRACTS Important Dates * Submission deadline for abstracts: 21 July, 2010 * Author Notification: 15 August, 2010 * Workshop: Saturday, 25 September, 2010 Scope * Tool demonstrations: proof assistants, logical frameworks, visualizers, etc. * Libraries for programming language metatheory * Novel formalization techniques * Investigation of formalization issues, especially with respect to variable binding * Examples of formalized programming language metatheory * Analysis and comparison of solutions to the POPLmark challenge * Proposals for new challenge problems that benchmark programming language work