The POPLmark Challenge

From POPLmark

The POPLmark Challenge is a concrete set of benchmarks intended both for measuring progress and for stimulating discussion and collaboration in mechanizing the metatheory of programming languages.

1 News
2 Vision
3 Challenge problems
4 Meetings
5 Solutions
6 Mailing List
7 Other Resources
8 People
9 Acknowledgement

[edit] News

[8 Nov 2007] André Hirschowitz and Marco Maggesi have posted an updated solution to part 1a.

[28 Sep 2007] There will be a workshop at POPL 2008 on Using Proof Assistants for Programming Language Research (or, How to write your next POPL paper in Coq).

[22 Feb 2007] The 2nd ACM SIGPLAN Workshop on Mechanizing Metatheory will be held this year at ICFP'07. The deadline for submitting abstracts is 18 June 2007.

[21 Jan 2007] Xavier Leroy has extended his solution to cover parts 2a and 3.

[19 Jan 2007] A solution by Wilmer Ricciotti in Matita has been posted.

[5 Jan 2007] A direct solution by Jevgenijs Sallinens has been posted.

[11 May 2006] You must have an account in order to edit the wiki, but account creation has been disabled due to spammers creating large numbers of accounts. If you'd like an account, send email to Brian Aydemir (baydemir [at] cis . upenn . edu) with your real name and a user name.

[edit] Vision

How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem.

It is is our hope that this wiki will be a resource for the communities as we work to educate everyone on the current state of the art in tools and techniques. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses.

[edit] Challenge problems

To gauge progress in mechanizing programming language metatheory, we issue here a set of challenge problems chosen to exercise many aspects of programming languages that are known to be difficult to formalize.

A description of the challenge problems: [pdf] [ps] [ps.gz]
A preliminary version of the F sub interpreter (written in OCaml): [tar.gz]
A set of test terms for Challenge 3: [tar.gz]

[edit] Meetings

The 2nd Workshop on Mechanizing Metatheory will be held on on October 4, 2007, in conjunction with ICFP 2007. The abstract submission deadline is June 18, 2007.

The 1st Workshop on Mechanizing Metatheory was held at ICFP 2006, on September 21, 2006. Slides from the workshop are available.

A "Progress on Poplmark" meeting was held on January 15th, 2006. Some of the people working actively on PoplMark gathered to discuss the solutions submitted so far. A transcript of the discussion and a few slides that people presented can be found on the ProgressMeeting06 page.

[edit] Solutions

The solutions we have received so far can be found on the submitted solutions page.

New solutions should be announced on the mailing list. (We can add appropriate sections and links to the submissions page for you, but feel free to do it yourself if you like.) Submissions should adhere to the following guidelines.

The formalization of the definition of F sub should be separated from the formalization of its metatheory. For example, the definitions of the subtyping relation, typing relation, and operational semantics should appear together rather than being separated by lemmas and theorems.
Code that is needed regardless of the particular object language being formalized should be separated from the code that is specific to F sub.
Any definitions, lemmas, theorems that correspond to ones from the challenge description, including the paper proofs, should be commented as such. These comments should also include (brief) justifications as to why the correspondence holds and what, if anything, had to be made explicit in going from the definitions to paper to the definitions in the formal environment.
We encourage developers to put up their own web pages, which we can link to, that provide code and describe their submissions.
As a convenience, we would appreciate it if developers could include appropriate line counts with their submissions; see the submissions page for exact counts we would like.