Back to Search
Start Over
A Solution to the P oplM ark Challenge Based on de Bruijn Indices.
- Source :
- Journal of Automated Reasoning; Oct2012, Vol. 49 Issue 3, p327-362, 36p
- Publication Year :
- 2012
-
Abstract
- The PoplMark challenge proposes a set of benchmarks intended to assess the usability of proof assistants in the context of research on programming languages. It is based on the metatheory of System F $_{\mathtt{<:}}$. We present a solution to the challenge using de Bruijn indices, developed with the Coq proof assistant. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 01687433
- Volume :
- 49
- Issue :
- 3
- Database :
- Complementary Index
- Journal :
- Journal of Automated Reasoning
- Publication Type :
- Academic Journal
- Accession number :
- 78322647
- Full Text :
- https://doi.org/10.1007/s10817-011-9230-5