POPLmark Reloaded

How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine checked proofs? POPLmark Reloaded, as the name suggests, follows up the original POPLmark Challenge by proposing a new collection of benchmark problems in mechanizing the meta-theory of programming languages, in order to compare and push the state of the art of proof assistants. We focus on proofs using logical relations and propose establishing strong normalization of a simply-typed lambda-calculus (and its extension with disjoint sums) with a proof by Kripke-style logical relations as a benchmark. More details in the paper "POPLMark Reloaded: Mechanizing Proofs by Logical Relations", please check it out at (DOI). Please cite it as:

@article{poplmark_reloaded,
 title =	 {POPLMark reloaded: Mechanizing proofs by logical
                  relations},
 volume =	 29,
 DOI =		 {10.1017/S0956796819000170},
 journal =	 {Journal of Functional Programming},
 publisher =	 {Cambridge University Press},
 author =	 {Abel, Andreas and Allais, Guillaume and Hameer,
                  Aliya and Pientka, Brigitte and Momigliano, Alberto
                  and Schäfer, Steven and Stark, Kathrin},
  year =	 2019,
  pages =	 {e19}
}

About the Challenge Problems

A pre-print of the paper: [PDF]
The appendix with the detailed proof of the challenge and its extension: [PDF]
You can browse the HTML of some solutions to the challenge and the code below.

Initial Solutions

We have supplemented the paper with a set of solutions of the basic challenge and its extension in Agda, Coq and Beluga. The community has already provided additional solutions in F* and Lean. Here's a summary:

System	Technique	STLC	STLC+
Agda	Generic syntax	Allais (code)	Allais (code)
Beluga	HOAS, well-typed	Hameer and Pientka (code)	Hameer and Pientka (code)
Coq	DB, well-scoped	Schaefer and Stark (code)	Schaefer and Stark (code)
Coq	DB, well-typed	Schaefer and Stark (code)	Schaefer and Stark (code)
F*	DB, well-typed	Sturm
Lean 3	DB, well-scoped	Mameche

More information about the F* solution can be found in Sebastian's MS thesis.

The Lean development provides a solution to the first variant of the POPLMark Reloaded challenge without an intermediate inductive characterisation of strong normalization.

Contributing

We welcome contributions from the community, in the form of solutions, or even as suggestions of future challenges. You can write to poplmarkreloaded@gmail.com or directly pull from the GitHub repo.

People

The POPLmark Reloaded team is:

Andreas Abel (Gothenburg University), Guillaume Allais (Radboud University), Aliya Hameer, Brigitte Pientka (Mcgill University), Alberto Momigliano (University of Milan), Steven Schaefer and Kathrin Stark (Saarland University).