Partial Type Equivalences for Verified Dependent Interoperability

Pierre-Evariste Dagand 1 Nicolas Tabareau 2 Éric Tanter 3
1 Whisper - Well Honed Infrastructure Software for Programming Environments and Runtimes
LIP6 - Laboratoire d'Informatique de Paris 6, Inria de Paris
2 ASCOLA - Aspect and composition languages
LINA - Laboratoire d'Informatique de Nantes Atlantique, Département informatique - EMN, Inria Rennes – Bretagne Atlantique
Abstract : Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, the dependent interoperability framework provides a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application. In this paper, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notion of partial type equivalences as a key foundation for dependent interoperability. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial equivalences between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.
Type de document :
Communication dans un congrès
ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. pp.298-310, <>. <10.1145/2951913.2951933>
Liste complète des métadonnées
Contributeur : Nicolas Tabareau <>
Soumis le : mercredi 25 janvier 2017 - 13:13:05
Dernière modification le : mardi 28 février 2017 - 17:14:06
Document(s) archivé(s) le : mercredi 26 avril 2017 - 15:39:03


Fichiers produits par l'(les) auteur(s)




Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter. Partial Type Equivalences for Verified Dependent Interoperability. ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming, Sep 2016, Nara, Japan. pp.298-310, <>. <10.1145/2951913.2951933>. <hal-01328012>



Consultations de
la notice


Téléchargements du document