Foundations of Dependent Interoperability

Pierre-Evariste Dagand 1 Nicolas Tabareau 2, 3 Éric Tanter 4
1 Whisper - Well Honed Infrastructure Software for Programming Environments and Runtimes
Inria de Paris, LIP6 - Laboratoire d'Informatique de Paris 6
2 GALLINETTE - GALLINETTE
LS2N - Laboratoire des Sciences du Numérique de Nantes, 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 article, 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 type-theoretic partial Galois connections as a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types. We explore the applicability of both monotone and antitone type-theoretic Galois connections in the setting of dependent interoperability. A monotone partial Galois connection enforces a translation of dependent types to runtime checks that are both sound and complete with respect to the invariants encoded by dependent types. Conversely, picking an antitone partial Galois connection instead lets us induce weaker, sound conditions that can amount to more efficient runtime checks. 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 connections 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 :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2018, 28, 〈10.1017/S0956796818000011〉
Liste complète des métadonnées

Littérature citée [50 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01629909
Contributeur : Pierre-Évariste Dagand <>
Soumis le : dimanche 17 décembre 2017 - 16:58:17
Dernière modification le : mercredi 11 juillet 2018 - 07:53:15

Fichier

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

Identifiants

Citation

Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter. Foundations of Dependent Interoperability. Journal of Functional Programming, Cambridge University Press (CUP), 2018, 28, 〈10.1017/S0956796818000011〉. 〈hal-01629909v2〉

Partager

Métriques

Consultations de la notice

491

Téléchargements de fichiers

143