Gradual Certified Programming in Coq

Éric Tanter 1 Nicolas Tabareau 2, 3
2 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : Expressive static typing disciplines are a powerful way to achieve high-quality software. However, the adoption cost of such techniques should not be under-estimated. Just like gradual typing allows for a smooth transition from dynamically-typed to statically-typed programs, it seems desirable to support a gradual path to certified program- ming. We explore gradual certified programming in Coq, providing the possibility to postpone the proofs of selected properties, and to check “at runtime” whether the properties actually hold. Casts can be integrated with the implicit coercion mechanism of Coq to support implicit cast insertion a` la gradual typing. Additionally, when extracting Coq functions to mainstream languages, our encoding of casts sup- ports lifting assumed properties into runtime checks. Much to our surprise, it is not necessary to extend Coq in any way to support gradual certified programming. A simple mix of type classes and axioms makes it possible to bring gradual certified programming to Coq in a straightforward manner.
Type de document :
Communication dans un congrès
11th ACM Dynamic Languages Symposium (DLS 2015), Oct 2015, Pittsburgh, United States. 2015, 〈10.1145/2816707.2816710〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01238774
Contributeur : Nicolas Tabareau <>
Soumis le : lundi 7 décembre 2015 - 10:19:46
Dernière modification le : vendredi 22 juin 2018 - 09:27:23

Lien texte intégral

Identifiants

Collections

Citation

Éric Tanter, Nicolas Tabareau. Gradual Certified Programming in Coq. 11th ACM Dynamic Languages Symposium (DLS 2015), Oct 2015, Pittsburgh, United States. 2015, 〈10.1145/2816707.2816710〉. 〈hal-01238774〉

Partager

Métriques

Consultations de la notice

321