×

Mechanized metatheory for the masses: the PoplMark challenge. (English) Zbl 1152.68516

Hurd, Joe (ed.) et al., Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22–25, 2005. Proceedings. Berlin: Springer (ISBN 3-540-28372-2/pbk). Lecture Notes in Computer Science 3603, 50-65 (2005).
Summary: How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs?
We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of the system \(F_{<:}\), a typed lambda-calculus with second-order polymorphism, subtyping, and records, these 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), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.
For the entire collection see [Zbl 1087.68005].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI