17.3.05
The POPLmark Challenge
Here's a cool idea who's time has come. My student Benjamin Kavanagh
is working on a closely related idea, a tool to support animation
and typesetting (but not proofs) for programming language semantics.
Kudos to the Penn/Cambridge team for formulating a crisp challenge,
an excellent model for promoting research.
The POPLmark Challenge
How close are we to a world where programming language papers are
routinely supported by machine-checked metatheory proofs, where
full-scale language definitions are expressed in machine-processed
mathematics, and where language implementations are directly tested
against those definitions?
To clarify the current state of the art, and to motivate further
research, we propose some concrete benchmarks for measuring progress.
Based on System Fsub, a typed lambda-calculus with second-order
polymorphism, subtyping, and records, the benchmarks embody many
aspects of programming languages that are challenging to formalize:
variable binding at both the term and type levels, syntactic forms
with variable numbers of components (including binders), proofs
demanding complex induction principles, and algorithmic questions.
To keep the challenge manageable, it is intermediate in scale between
`toy' calculi and full programming languages.
The challenge problems are available from the web page
http://www.cis.upenn.edu/group/proj/plclub/mmm/,
with informal definitions of syntax and semantics, hand proofs of the
metatheoretic results, and a prototype implementation.
We encourage users and developers of automated reasoning tools to
attempt the challenges and send the results to the POPLmark mailing
list (from that same web page), which will provide a forum for debate.
Queries and clarifications should also be discussed there. The
POPLmark team can also be mailed directly at provers@lists.seas.upenn.edu.
We are not ourselves automated reasoning experts but rather potential
users; our impression is that current tools are _almost_ at the point
where they can be used routinely. It's time to bring mechanized
metatheory to the masses - go to it!
Peter, for the POPLmark team:
Brian Aydemir, Aaron Bohannon, Matthew Fairbairn, Nathan Foster,
Benjamin Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey
Washburn, Stephanie Weirich, and Steve Zdancewic
is working on a closely related idea, a tool to support animation
and typesetting (but not proofs) for programming language semantics.
Kudos to the Penn/Cambridge team for formulating a crisp challenge,
an excellent model for promoting research.
The POPLmark Challenge
How close are we to a world where programming language papers are
routinely supported by machine-checked metatheory proofs, where
full-scale language definitions are expressed in machine-processed
mathematics, and where language implementations are directly tested
against those definitions?
To clarify the current state of the art, and to motivate further
research, we propose some concrete benchmarks for measuring progress.
Based on System Fsub, a typed lambda-calculus with second-order
polymorphism, subtyping, and records, the benchmarks embody many
aspects of programming languages that are challenging to formalize:
variable binding at both the term and type levels, syntactic forms
with variable numbers of components (including binders), proofs
demanding complex induction principles, and algorithmic questions.
To keep the challenge manageable, it is intermediate in scale between
`toy' calculi and full programming languages.
The challenge problems are available from the web page
http://www.cis.upenn.edu/group/proj/plclub/mmm/,
with informal definitions of syntax and semantics, hand proofs of the
metatheoretic results, and a prototype implementation.
We encourage users and developers of automated reasoning tools to
attempt the challenges and send the results to the POPLmark mailing
list (from that same web page), which will provide a forum for debate.
Queries and clarifications should also be discussed there. The
POPLmark team can also be mailed directly at provers@lists.seas.upenn.edu.
We are not ourselves automated reasoning experts but rather potential
users; our impression is that current tools are _almost_ at the point
where they can be used routinely. It's time to bring mechanized
metatheory to the masses - go to it!
Peter, for the POPLmark team:
Brian Aydemir, Aaron Bohannon, Matthew Fairbairn, Nathan Foster,
Benjamin Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey
Washburn, Stephanie Weirich, and Steve Zdancewic
