Mtac: A monad for typed tactic programming in Coq
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 24112735
- Type
- D - Journal article
- DOI
-
10.1017/S0956796815000118
- Title of journal
- Journal of Functional Programming
- Article number
- e12
- First page
- -
- Volume
- 25
- Issue
- -
- ISSN
- 0956-7968
- Open access status
- Out of scope for open access requirements
- Month of publication
- August
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
4
- Research group(s)
-
-
- Citation count
- 10
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper introduced a new proof-automation language for the Coq proof assistant. It is significant because Coq is the basis for some of the largest machine-checked proofs (including the Compcert verified C compiler and the machine-checked proof of the Four Colour Theorem), and as the scale of the attempted proofs has grown the inadequacies of the existing tactic languages have grown harder to bear. This paper led directly to better unification algorithms for Coq (now adopted), and had a large influence on the design of Ltac2, Coq's latest tactic language.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -