Submitted solutions
From POPLmark
This page summarizes the submissions and solutions for The POPLmark Challenge; each submission also has a page dedicated to it that includes commentary (when available). Other related pages include: the description of the challenge problems, and how to submit a solution.
We currently have submissions from the following individuals and groups (names link to pages on their submission):
- Stefan Berghofer
- Arthur Charguéraud (de Bruijn indices)
- Arthur Charguéraud (locally nameless)
- Adam Chlipala
- Group from CMU (Michael Ashley-Rollman, Karl Crary, and Robert Harper)
- Matthew Fairbairn
- André Hirschowitz and Marco Maggesi
- Xavier Leroy
- Jevgenijs Sallinens
- Aaron Stump
- Christian Urban et al.
- Jérôme Vouillon
- Hongwei Xi
- Wilmer Ricciotti
- Andrew Gacek
Parts of the challenge addressed by each submission:
| 1a | 1b | 2a | 2b | 3 | Commented | |
|---|---|---|---|---|---|---|
| Berghofer | Y | Y | Y | Y | Y | |
| Charguéraud (de Bruijn indices) | Y | Y | ||||
| Charguéraud (locally nameless) | Y | Y | ||||
| Adam Chlipala | Y | Y | ||||
| CMU | Y | Y | Y | Y | Y | |
| Fairbairn | Y | |||||
| Hirschowitz and Maggesi | Y | minimally | ||||
| Leroy | Y | Y | Y | Y | ||
| Ricciotti | Y | |||||
| Sallinens | Y | Y | minimally | |||
| Stump | Y | Y | ||||
| Urban et al. | Y | Y | ||||
| Vouillon | Y | Y | Y | Y | Y | |
| Xi | Y | Y | ||||
| Gacek | Y | Y |
Summary of the encoding techniques and proof assistants / theorem provers used by the submissions:
| Alpha Prolog | Coq | Twelf | ATS | Isabelle/HOL | Matita | Abella | |
|---|---|---|---|---|---|---|---|
| De Bruijn indices | Vouillon, Sallinens, Charguéraud (a) |
Berghofer | |||||
| HOAS | CMU | Gacek | |||||
| Locally nameless | Chlipala, Leroy, Charguéraud (b) |
Ricciotti | |||||
| Nominal | Fairbairn | Urban et al. | |||||
| Named variables | Stump | ||||||
| Hybrid | Xi | ||||||
| Nested datatypes | Hirschowitz and Maggesi |
