Document Open Access Logo

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Author Meven Lennon-Bertrand

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.24.pdf
  • Filesize: 0.81 MB
  • 19 pages

Document Identifiers

Author Details

Meven Lennon-Bertrand
  • LS2N, Université de Nantes - Gallinette Project Team, Inria, France

Acknowledgements

Many thanks to Matthieu Sozeau for his help with MetaCoq and its nasty inductives, and to Chantal Keller, Nicolas Tabareau and the anonymous reviewers for their helpful comments on earlier versions of this article.

Cite As Get BibTex

Meven Lennon-Bertrand. Complete Bidirectional Typing for the Calculus of Inductive Constructions. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.24

Abstract

This article presents a bidirectional type system for the Calculus of Inductive Constructions (CIC). The key property of the system is its completeness with respect to the usual undirected one, which has been formally proven in Coq as a part of the MetaCoq project. Although it plays an important role in an ongoing completeness proof for a realistic typing algorithm, the interest of bidirectionality is wider, as it gives insights and structure when trying to prove properties on CIC or design variations and extensions. In particular, we put forward constrained inference, an intermediate between the usual inference and checking judgements, to handle the presence of computation in types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Bidirectional Typing
  • Calculus of Inductive Constructions
  • Coq
  • Proof Assistants

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel. Towards normalization by evaluation for the βη-calculus of constructions. In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings, volume 6009 of Lecture Notes in Computer Science, pages 224-239. Springer-Verlag, 2010. URL: https://doi.org/10.1007/978-3-642-12251-4.
  2. Andreas Abel and Thorsten Altenkirch. A partial type checking algorithm for type:type. Electronic Notes in Theoretical Computer Science, 229(5):3-17, 2011. Proceedings of the Second Workshop on Mathematically Structured Functional Programming (MSFP 2008). URL: https://doi.org/10.1016/j.entcs.2011.02.013.
  3. Andreas Abel and Thierry Coquand. Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Fundamenta Informaticae, 77(4):345-395, 2007. TLCA'05 special issue. Google Scholar
  4. Andreas Abel, Thierry Coquand, and Peter Dybjer. Verifying a semantic βη-conversion test for Martin-Löf type theory. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction, pages 29-56, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  5. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., December 2017. URL: https://doi.org/10.1145/3158111.
  6. Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau. Setoid type theory - a syntactic translation. In MPC 2019 - 13th International Conference on Mathematics of Program Construction, volume 11825 of LNCS, pages 155-196. Springer, October 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_7.
  7. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science, Volume 8, Issue 1, 2012. URL: https://doi.org/10.2168/LMCS-8(1:18)2012.
  8. Henk Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science. Oxford Universiy Press, 1992. Google Scholar
  9. Andrej Bauer, Philipp G. Haselwarter, and Peter LeFanu Lumsdaine. A general definition of dependent type theories. Preprint, 2020. URL: http://arxiv.org/abs/2009.05539.
  10. Jesper Cockx, Nicolas Tabareau, and Théo Winterhalter. The Taming of the Rew: A Type Theory with Computational Assumptions. Proceedings of the ACM on Programming Languages, 2021. URL: https://doi.org/10.1145/3434341.
  11. Thierry Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1), 1996. URL: https://doi.org/10.1016/0167-6423(95)00021-6.
  12. Trevor Jim. What are principal typings and what are they good for? In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '96, page 42–53, New York, NY, USA, 1996. Association for Computing Machinery. URL: https://doi.org/10.1145/237721.237728.
  13. Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. Gradualizing the calculus of inductive constructions. Preprint, 2020. URL: http://arxiv.org/abs/2011.10618.
  14. Conor McBride. I got plenty o' nuttin'. In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella, editors, A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 207-233. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_12.
  15. Conor McBride. Basics of bidirectionalism. Blog post, August 2018. URL: https://pigworker.wordpress.com/2018/08/06/basics-of-bidirectionalism/.
  16. Conor McBride. Check the box! In 25th International Conference on Types for Proofs and Programs, June 2019. Google Scholar
  17. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007. Google Scholar
  18. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option an exceptional type theory. In ESOP 2018 - 27th European Symposium on Programming, volume 10801 of LNCS, pages 245-271, Thessaloniki, Greece, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
  19. R. Pollack. Typechecking in Pure Type Systems. In Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, pages 271-288, June 1992. URL: http://homepages.inf.ed.ac.uk/rpollack/export/BaastadTypechecking.ps.gz.
  20. Amokrane Saïbi. Typing algorithm in type theory with inheritance. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’97, 1997. URL: https://doi.org/10.1145/263699.263742.
  21. Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, 1st Summit on Advances in Programming Languages (SNAPL 2015), volume 32 of Leibniz International Proceedings in Informatics (LIPIcs), pages 274-293. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.SNAPL.2015.274.
  22. Matthieu Sozeau. Subset coercions in coq. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, pages 237-252, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-74464-1_16.
  23. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, February 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
  24. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, pages 1-28, January 2020. URL: https://doi.org/10.1145/3371076.
  25. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 499-514, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-08970-6_32.
  26. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  27. Amin Timany and Matthieu Sozeau. Cumulative Inductive Types In Coq. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1-16, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.29.
  28. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Proc. ACM Program. Lang., 3(ICFP), July 2019. URL: https://doi.org/10.1145/3341691.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact