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.
Supplemental Material
Available for Download
This is an expanded version of the technical sections for the paper by the same title. This contains extended versions of figured and proofs, and additional discussions and explanations.
- Amal Ahmed. 2015. Verified Compilers for a Multi-language World. In Summit on Advances in Programming Languages (SNAPL), Vol. 32.Google Scholar
- Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Amal Ahmed and Matthias Blume. 2011. An Equivalence-preserving CPS Translation Via Multi-language Semantics. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundamenta Informaticae 77, 4 (Dec. 2007). Google ScholarDigital Library
- 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 Scholar
- Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Transactions on Programming Languages and Systems (TOPLAS) 37, 2 (April 2015). Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Gilles Barthe and Tarmo Uustalu. 2002. CPS Translating Inductive and Coinductive Types. In Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM). Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- William J. Bowman and Amal Ahmed. 2015. Noninterference for Free. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Thierry Coquand. 1986. An Analysis of Girard's Paradox. In Symposium on Logic in Computer Science (LICS). https://hal.inria.fr/inria-00076023Google Scholar
- Eduardo Giménez. 1995. Codifying Guarded Definitions with Recursive Schemes. In International Workshop on Types for Proofs and Programs (TYPES). Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Hugo Herbelin. 2005. On the Degeneracy of ?-types in Presence of Computational Classical Logic. In International Conference on Typed Lambda Calculi and Applications. Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 Scholar
- Xavier Leroy. 2009. A Formally Verified Compiler Back-end. Journal of Automated Reasoning 43, 4 (Nov. 2009). Google ScholarDigital Library
- Zhaohui Luo. 1989. ECC, an Extended Calculus of Constructions. In Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- 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 Scholar
- Yasuhiko Minamide, Greg Morrisett, and Robert Harper. 1996. Typed Closure Conversion. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In International Conference on Typed Lambda Calculi and Applications (TLCA). Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully Abstract Compilation Via Universal Embedding. In International Conference on Functional Programming (ICFP). Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In European Symposium on Programming (ESOP). Google ScholarDigital Library
- 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 ScholarDigital Library
- Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- 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 Scholar
Index Terms
Typed closure conversion for the calculus of constructions
Recommendations
Type-preserving CPS translation of Σ and Π types is not not possible
Dependently typed languages such as Coq are used to specify and prove functional correctness of source programs, but what we ultimately need are guarantees about correctness of compiled code. By preserving dependent types through each compiler pass, we ...
Typed closure conversion
POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesClosure conversion is a program transformation used by compilers to separate code from data. Previous accounts of closure conversion use only untyped target languages. Recent studies show that translating to typed target languages is a useful ...
Typed closure conversion for the calculus of constructions
PLDI '18Dependently 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 ...
Comments