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.
Type de document :
Communication dans un congrès
Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.19-34, 2013, LNCS. <10.1007/978-3-642-39634-2_5>
Liste complète des métadonnées

https://hal.inria.fr/hal-00816703
Contributeur : Assia Mahboubi <>
Soumis le : lundi 29 avril 2013 - 16:21:23
Dernière modification le : jeudi 9 février 2017 - 15:48:21
Document(s) archivé(s) le : lundi 19 août 2013 - 09:50:24

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Assia Mahboubi, Enrico Tassi. Canonical Structures for the working Coq user. Sandrine Blazy and Christine Paulin and David Pichardie. ITP 2013, 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.19-34, 2013, LNCS. <10.1007/978-3-642-39634-2_5>. <hal-00816703v2>

Partager

Métriques

Consultations de
la notice

1052

Téléchargements du document

760