Canonical Structures for the working Coq user

Abstract : This paper provides a gentle introduction to the art of programming type inference with the mechanism of Canonical Structures. Programmable type inference has been one of the key ingredients for the successful formalization of the Odd Order Theorem using the Coq proof assistant. The paper concludes comparing the language of Canonical Structures to the one of Type Classes and Unification Hints.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-00816703
Contributor : Assia Mahboubi <>
Submitted on : Monday, April 29, 2013 - 4:21:23 PM
Last modification on : Monday, February 12, 2018 - 1:26:02 PM
Long-term archiving on : Monday, August 19, 2013 - 9:50:24 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Assia Mahboubi, Enrico Tassi. Canonical Structures for the working Coq user. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.19-34, ⟨10.1007/978-3-642-39634-2_5⟩. ⟨hal-00816703v2⟩

Share

Metrics

Record views

1566

Files downloads

1713