Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-24T22:58:48.088Z Has data issue: false hasContentIssue false
  • English
  • Français

Foundations of dependent interoperability

Part of: JFP Research Articles

Published online by Cambridge University Press:  13 March 2018

PIERRE-ÉVARISTE DAGAND ,
NICOLAS TABAREAU  and
ÉRIC TANTER
PIERRE-ÉVARISTE DAGAND
Affiliation:
Sorbonne Universités, UPMC Univ Paris 06, CNRS, INRIA, LIP6 UMR 7606, Paris, France (e-mail: [email protected])
NICOLAS TABAREAU
Affiliation:
INRIA, Paris, France (e-mail: [email protected])
ÉRIC TANTER
Affiliation:
PLEIAD Lab, Computer Science Dept (DCC), University of Chile, Santiago, Chile (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 notions 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 type-theoretic Galois connections and anticonnections in the setting of dependent interoperability. A 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 anticonnection 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
Articles
Information
Journal of Functional Programming , Volume 28 , 2018 , e9
Copyright
Copyright © Cambridge University Press 2018 

References

Altenkirch, T., McBride, C. & Swierstra, W. (2007) Observational equality, now! In Proceedings of the ACM Workshop on Programming Languages Meets Program Verification (PLPV '07), pp. 57–68.Google Scholar
Awodey, S. & Bauer, A. (2004) Propositions as [types]. J. Log. Comput. 14 (4), 447–471.Google Scholar
Bañados, F., Garcia, R. & Tanter, É. (2014) A theory of gradual effect systems. In Proceedings of the 19th ACM Sigplan Conference on Functional Programming (ICFP '14). Gothenburg, Sweden: ACM, pp. 283–295.Google Scholar
Bañados Schwerter, F., Garcia, R. & Tanter, É. (2016) Gradual type-and-effect systems. J. Funct. Program. 26, 19:1–19:69.Google Scholar
Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. & Spitters, B. (2017) The HoTT library: A formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '17). Paris, France: ACM, pp. 164–172.Google Scholar
Boulier, S., Pédrot, P.-M. & Tabareau, N. (2017) The next 700 syntactical models of type theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP '17). Paris, France: ACM, pp. 182–194.Google Scholar
Brady, E., McBride, C. & McKinna, J. (2004) Inductive families need not store their indices. In Types for Proofs and Programs, Berardi, Stefano, Coppo, Mario, & Damiani, Ferruccio (eds), Lecture Notes in Computer Science, vol. 3085. Springer-Verlag, pp. 115–129.CrossRefGoogle Scholar
Chlipala, A. (2013) Certified Programming with Dependent Types. MIT Press.Google Scholar
Clairambault, P. (2012) Isomorphisms of types in the presence of higher-order references (extended version) Logical Methods Comput. Sci. 8 (3). https://www.cambridge.org/core/journals/journal-of-functional-programming/article/div-classtitleeliminating-dependent-pattern-matching-without-kdiv/4BC4EA2D02D801E5ABED264FE5FB177A/share/4b301f760a5075bf8f56a06fd80f701817f417c1 Google Scholar
Cockx, J., Devriese, D. & Piessens, F. (2016) Eliminating dependent pattern matching without K. J. Funct. Program. 26, e16.CrossRefGoogle Scholar
Cohen, C., Dénès, M. & Mörtberg, A. (2013) Refinements for free! In Proceedings of the 3rd International Conference on Certified Programs and Proofs (CPP '13), pp. 147–162.Google Scholar
Cosmo, R. D. (2005) A short survey of isomorphisms of types. Math. Struct. Comput. Sci. 15 (5), 825–838.Google Scholar
Dagand, P.-É. & McBride, C. (2012) Transporting functions across ornaments. In Proceedings of the 17th ACM Sigplan Conference on Functional Programming (ICFP '12). Copenhagen, Denmark: ACM, pp. 103–114.Google Scholar
Dagand, P.-E., Tabareau, N., & Tanter, É. (2016) Partial type equivalences for verified dependent interoperability. In Proceedings of the 21st ACM Sigplan Conference on Functional Programming (ICFP '16). Nara, Japan: ACM, pp. 298–310.Google Scholar
Delaware, B., Pit-Claudel, C., Gross, J. & Chlipala, A. (2015) Fiat: Deductive synthesis of abstract data types in a proof assistant. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). Mumbai, India: ACM, pp. 689–700.Google Scholar
Disney, T. & Flanagan, C. (2011) Gradual information flow typing. In Proceedings of International Workshop on Scripts to Programs.Google Scholar
Fennell, L., & Thiemann, P. (2013) Gradual security typing with references. In Proceedings of the 26th Computer Security Foundations Symposium (CSF), pp. 224–239.CrossRefGoogle Scholar
Findler, R. B., & Felleisen, M. (2002) Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN Conference on Functional Programming (ICFP '02). Pittsburgh, PA, USA: ACM. pp. 48–59.Google Scholar
Garcia, R., Clark, A. M. & Tanter, É. (2016) Abstracting gradual typing. In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '16). St Petersburg, FL, USA: ACM, pp. 429–442.Google Scholar
Gonthier, G. & Mahbouhi, A. (2010) An introduction to small scale reflection in Coq. J. Formalized Reason. 3 (2), 95–152.Google Scholar
Hofmann, M. & Streicher, T. (1994) The groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic In Computer Science (LICS '94). IEEE Computer Society Press, pp. 208–212.Google Scholar
Hyland, J. M. E. (1991) First steps in synthetic domain theory. In Proceedings of the International Conference on Category Theory. Como, Italy: Springer-Verlag, pp. 131–156.Google Scholar
Knowles, K. & Flanagan, C. (2010) Hybrid type checking. ACM Trans. Program. Lang. Syst. 32 (2), Article no.6.Google Scholar
Ko, H.-S., & Gibbons, J. (2013) Relational algebraic ornaments. In Proceedings of the ACM SIGPLAN Workshop on Dependently Typed Programming (DTP '13). ACM, pp. 37–48.Google Scholar
Laurent, O. (2005) Classical isomorphisms of types. Math. Struct. Comput. Sci. 15 (5), 969–1004.Google Scholar
Lehmann, N. & Tanter, É. (2017) Gradual refinement types. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '17). Paris, France: ACM, pp. 775–788.Google Scholar
Letouzey, P. (2004) Programmation fonctionnelle certifiée – l'extraction de programmes dans l'assistant Coq. Ph.D. thesis, Université Paris-Sud.Google Scholar
Levy, P. B. (2017) Contextual isomorphisms. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '17). Paris, France: ACM, pp. 400–414.Google Scholar
Matthews, J., & Findler, R. B. (2007) Operational semantics for multi-language programs. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07). Nice, France: ACM, pp. 3–10.Google Scholar
McBride, C. (2000) Elimination with a motive. In Proceedings of the International Workshop on Types for Proofs and Programs (types 2000), pp. 197–216.Google Scholar
McBride, C. (2010) Ornamental Algebras, Algebraic Ornaments. Technical Report, University of Strathclyde.Google Scholar
McKinna, J. (2006) Why dependent types matter. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06). Charleston, South Carolina, USA: ACM, p. 1.CrossRefGoogle Scholar
Mishra-Linger, N. & Sheard, T. (2008) Erasure and polymorphism in pure type systems. In Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS '08). Lecture Notes in Computer Science, vol. 4962. Springer-Verlag, pp. 350–364.Google Scholar
Osera, P.-M., Sjöberg, V. & Zdancewic, S. (2012) Dependent interoperability. In Proceedings of the 6th Workshop on Programming Languages Meets Program Verification (PLPV '12). ACM, pp. 3–14.CrossRefGoogle Scholar
Ou, X., Tan, G., Mandelbaum, Y. & Walker, D. (2004) Dynamic typing with dependent types. In Proceedings of the ifip International Conference on Theoretical Computer Science, pp. 437–450.Google Scholar
Rondon, P. M., Kawaguchi, M. & Jhala, R. (2008) Liquid types. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008), Gupta, Rajiv, & Amarasinghe, Saman P. (eds). ACM, pp. 159–169.Google Scholar
Sekiyama, T., Nishida, Y., & Igarashi, A. (2015) Manifest contracts for datatypes. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). Mumbai, India: ACM, pp. 195–207.Google Scholar
Siek, J. & Taha, W. (2006) Gradual typing for functional languages. In Proceedings of the Scheme and Functional Programming Workshop, pp. 81–92.Google Scholar
Siek, J. G., Vitousek, M. M., Cimini, M. & Boyland, J. T. (2015) Refined criteria for gradual typing. In Proceedings of the 1st Summit on Advances in Programming Languages (SNAPL '15), pp. 274–293.Google Scholar
Sozeau, M. (2010) Equations: A dependent pattern-matching compiler. In Proceedings of the 1st International Conference on Interactive Theorem proving (ITP '10), Kaufmann, M. & Paulson, L. C. (eds). Lecture Notes in Computer Science, vol. 6172. Springer-Verlag, pp. 419–434.Google Scholar
Sozeau, M. & Oury, N. (2008) First-class type classes. In Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics, pp. 278–293.Google Scholar
Swierstra, W. & Alpuim, J. (2016) From proposition to program – embedding the refinement calculus in Coq. In Proceedings of the 13th International Symposium on Functional and Logic Programming (FLOPS '16), pp. 29–44.Google Scholar
Tanter, É. & Tabareau, N. (2015) Gradual certified programming in Coq. In Proceedings of the 11th ACM Dynamic Languages Symposium (DLS '15). Pittsburgh, PA, USA: ACM, pp. 26–40.Google Scholar
The Coq Development Team. (2016) The Coq Proof Assistant Reference Manual. Version 8.6.Google Scholar
The Univalent Foundations Program. (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http://homotopytypetheory.org/book.Google Scholar
Thiemann, P. & Fennell, L. (2014) Gradual typing for annotated type systems. In Proceedings of the 23rd European Symposium on Programming Languages and Systems (ESOP '14), Shao, Z. (ed). Lecture Notes in Computer Science, vol. 8410. Grenoble, France: Springer-Verlag, pp. 47–66.Google Scholar
Toro, M. & Tanter, É. (2015) Customizable gradual polymorphic effects for Scala. In Proceedings of the 30th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA '15). Pittsburgh, PA, USA: ACM, pp. 935–953.Google Scholar
Wadler, P. & Blott, S. (1989) How to make ad-hoc polymorphism less ad hoc. In Proceedings of the 16th ACM Symposium on Principles of Programming Languages (POPL '89). Austin, TX, USA: ACM, pp. 60–76.Google Scholar
Williams, T., Dagand, P.-É. & Rémy, D. (2014) Ornaments in practice. In Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming (WGP 2014), Magalhães, J. P. & Rompf, T (eds). Gothenburg, Sweden: ACM, pp. 15–24.Google Scholar
Xi, H. & Pfenning, F. (1998) Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '98). ACM, pp. 249–257.Google Scholar
Zimmermann, T. & Herbelin, H. (2015) Automatic and Transparent Transfer of Theorems Along Isomorphisms in the Coq Proof Assistant. arXiv:1505.05028v4.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.