skip to main content
10.1145/3192366.3192372acmconferencesArticle/Chapter ViewAbstractPublication PagespldiConference Proceedingsconference-collections
research-article

Typed closure conversion for the calculus of constructions

Published:11 June 2018Publication History

ABSTRACT

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms.

We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs (Σ types)—a subset of the core language of Coq—to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.

Skip Supplemental Material Section

Supplemental Material

p797-bowman.webm

References

  1. Amal Ahmed. 2015. Verified Compilers for a Multi-language World. In Summit on Advances in Programming Languages (SNAPL), Vol. 32.Google ScholarGoogle Scholar
  2. Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming (ICFP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Amal Ahmed and Matthias Blume. 2011. An Equivalence-preserving CPS Translation Via Multi-language Semantics. In International Conference on Functional Programming (ICFP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundamenta Informaticae 77, 4 (Dec. 2007). Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Abhishek Anand, A. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A Verified Compiler for Coq. In International Workshop on Coq for Programming Languages (CoqPL). http://www.cs.princeton.edu/~appel/papers/certicoq-coqpl.pdfGoogle ScholarGoogle Scholar
  6. Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Transactions on Programming Languages and Systems (TOPLAS) 37, 2 (April 2015). Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Bruno Barras and Bruno Bernardo. 2008. The Implicit Calculus of Constructions As a Programming Language with Dependent Types. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Symposium on Principles of Programming Languages (POPL). Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Gilles Barthe, John Hatcliff, and Morten Heine B. Sørensen. 1999. CPS Translations and Applications: The Cube and Beyond. Higher-Order and Symbolic Computation 12, 2 (Sept. 1999). Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Gilles Barthe and Tarmo Uustalu. 2002. CPS Translating Inductive and Coinductive Types. In Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM). Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Jean-philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for Free: Parametricity for Dependent Types. Journal of Functional Programming (JFP) 22, 02 (March 2012). Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017. The Next 700 Syntactical Models of Type Theory. In Conference on Certified Programs and Proofs (CPP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. William J. Bowman and Amal Ahmed. 2015. Noninterference for Free. In International Conference on Functional Programming (ICFP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. William J. Bowman and Amal Ahmed. 2018. Typed Closure Conversion for the Calculus of Constructions (Technical Appendix). Technical Report. https://www.williamjbowman.com/resources/cccc-techrpt.pdfGoogle ScholarGoogle Scholar
  15. William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2018. Type-preserving CPS Translation of S and ? Types Is Not Not Possible. Proceedings of the ACM on Programming Languages (PACMPL) 2, POPL (Jan. 2018). Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Juan Chen, Ravi Chugh, and Nikhil Swamy. 2010. Type-preserving Compilation of End-to-end Verification of Security Enforcement. In International Conference on Programming Language Design and Implementation (PLDI). Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Thierry Coquand. 1986. An Analysis of Girard's Paradox. In Symposium on Logic in Computer Science (LICS). https://hal.inria.fr/inria-00076023Google ScholarGoogle Scholar
  18. Eduardo Giménez. 1995. Codifying Guarded Definitions with Recursive Schemes. In International Workshop on Types for Proofs and Programs (TYPES). Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Benjamin Grégoire and Jorge Luis Sacchini. 2010. On Strong Normalization of the Calculus of Constructions with Type-based Termination. In International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (newman) Wu, Shu-chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Symposium on Principles of Programming Languages (POPL). Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Symposium on Operating Systems Design and Implementation (OSDI). https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. Hugo Herbelin. 2005. On the Degeneracy of ?-types in Presence of Computational Classical Logic. In International Conference on Typed Lambda Calculi and Applications. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. James G. Hook and Douglas J. Howe. 1986. Impredicative Strong Existential Equivalent to Type:Type. Technical Report. Cornell University. http://hdl.handle.net/1813/6600 Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight Verification of Separate Compilation. In Symposium on Principles of Programming Languages (POPL). Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In International Workshop on Computer Science Logic (CSL). https://hal.inria.fr/hal-00730913Google ScholarGoogle Scholar
  26. Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In International Workshop on Computer Science Logic (CSL).Google ScholarGoogle Scholar
  27. Xavier Leroy. 2009. A Formally Verified Compiler Back-end. Journal of Automated Reasoning 43, 4 (Nov. 2009). Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. Zhaohui Luo. 1989. ECC, an Extended Calculus of Constructions. In Symposium on Logic in Computer Science (LICS). Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Conor McBride. 2016. I Got Plenty o' Nuttin'. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday.Google ScholarGoogle Scholar
  30. Yasuhiko Minamide, Greg Morrisett, and Robert Harper. 1996. Typed Closure Conversion. In Symposium on Principles of Programming Languages (POPL). Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In International Conference on Typed Lambda Calculi and Applications (TLCA). Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. Richard Nathan Mishra-linger. 2008. Irrelevance, Polymorphism, and Erasure in Type Theory. Ph.D. Dissertation. Portland State University. http://pdxscholar.library.pdx.edu/cgi/viewcontent.cgi?article=3678&context=open_access_etdsGoogle ScholarGoogle Scholar
  34. Greg Morrisett and Robert Harper. 1998. Typed Closure Conversion for Recursively-defined Functions. Electronic Notes in Theoretical Computer Science 10 (June 1998), 230-241. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. 1998. From System F to Typed Assembly Language. In Symposium on Principles of Programming Languages (POPL). Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: A Compositionally Verified Compiler for a Higher-order Imperative Language. In International Conference on Functional Programming (ICFP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully Abstract Compilation Via Universal Embedding. In International Conference on Functional Programming (ICFP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. 2017. Parametric Quantifiers for Dependent Type Theory. Proceedings of the ACM on Programming Languages (PACMPL) 1, ICFP (Aug. 2017). Google ScholarGoogle ScholarDigital LibraryDigital Library
  39. Daniel Patterson and Amal Ahmed. 2017. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In Summit on Advances in Programming Languages (SNAPL).Google ScholarGoogle Scholar
  40. Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. 2017. FunTAL: Reasonably Mixing a Functional Language with Assembly. In International Conference on Programming Language Design and Implementation (PLDI). Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In European Symposium on Programming (ESOP). Google ScholarGoogle ScholarDigital LibraryDigital Library
  42. Zhong Shao, Valery Trifonov, Bratin Saha, and Nikolaos Papaspyrou. 2005. A Type System for Certified Binaries. ACM Transactions on Programming Languages and Systems (TOPLAS) 27, 1 (Jan. 2005). Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Symposium on Principles of Programming Languages (POPL). Google ScholarGoogle ScholarDigital LibraryDigital Library
  44. The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. https://web.archive.org/web/20170109225110/https://coq.inria.fr/doc/Reference-Manual006.htmlGoogle ScholarGoogle Scholar

Index Terms

  1. Typed closure conversion for the calculus of constructions

            Recommendations

            Comments

            Login options

            Check if you have access through your login credentials or your institution to get full access on this article.

            Sign in
            • Published in

              cover image ACM Conferences
              PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
              June 2018
              825 pages
              ISBN:9781450356985
              DOI:10.1145/3192366

              Copyright © 2018 ACM

              Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

              Publisher

              Association for Computing Machinery

              New York, NY, United States

              Publication History

              • Published: 11 June 2018

              Permissions

              Request permissions about this article.

              Request Permissions

              Check for updates

              Qualifiers

              • research-article

              Acceptance Rates

              Overall Acceptance Rate406of2,067submissions,20%

              Upcoming Conference

              PLDI '24

            PDF Format

            View or Download as a PDF file.

            PDF

            eReader

            View online with eReader.

            eReader