Document Open Access Logo

For the Metatheory of Type Theory, Internal Sconing Is Enough

Authors Rafaël Bocquet , Ambrus Kaposi , Christian Sattler

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.18.pdf
  • Filesize: 0.87 MB
  • 23 pages

Document Identifiers

Author Details

Rafaël Bocquet
  • Eötvös Loránd University, Budapest, Hungary
Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
Christian Sattler
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Kaposi, Ambrus: Supported by the Bolyai Fellowship of the Hungarian Academy of Sciences and by the "Application Domain Specific Highly Reliable IT Solutions" project of the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 funding scheme.

Cite AsGet BibTex

Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the Metatheory of Type Theory, Internal Sconing Is Enough. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 18:1-18:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.18

Abstract

Metatheorems about type theories are often proven by interpreting the syntax into models constructed using categorical gluing. We propose to use only sconing (gluing along a global section functor) instead of general gluing. The sconing is performed internally to a presheaf category, and we recover the original glued model by externalization. Our method relies on constructions involving two notions of models: first-order models (with explicit contexts) and higher-order models (without explicit contexts). Sconing turns a displayed higher-order model into a displayed first-order model. Using these, we derive specialized induction principles for the syntax of type theory. The input of such an induction principle is a boilerplate-free description of its motives and methods, not mentioning contexts. The output is a section with computation rules specified in the same internal language. We illustrate our framework by proofs of canonicity and normalization for type theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • presheaves
  • canonicity
  • normalization
  • sconing
  • gluing

Metrics

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

Related Versions

References

  1. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL):23:1-23:29, 2018. URL: https://doi.org/10.1145/3158111.
  2. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter T. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, CTCS '95, Cambridge, UK, August 7-11, 1995, Proceedings, volume 953 of Lecture Notes in Computer Science, pages 182-199. Springer, 1995. URL: https://doi.org/10.1007/3-540-60164-3_27.
  3. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for a polymorphic system. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 98-106. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561309.
  4. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.6.
  5. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 18-29, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837638.
  6. Thorsten Altenkirch, Ambrus Kaposi, and Michael Shulman. Towards higher observational type theory. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022). University of Nantes, 2022. URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_37.pdf.
  7. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. CoRR, abs/1705.03307, 2019. URL: https://arxiv.org/abs/1705.03307.
  8. Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, 28(2):241-286, 2018. URL: https://doi.org/10.1017/S0960129516000268.
  9. Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Proofs for free - parametricity for dependent types. Journal of Functional Programming, 22(02):107-152, 2012. URL: https://doi.org/10.1017/S0956796812000056.
  10. Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. Relative induction principles for type theories. CoRR, abs/2102.11649, 2021. URL: https://arxiv.org/abs/2102.11649.
  11. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. CoRR, abs/1904.00827, 2019. URL: https://arxiv.org/abs/1904.00827.
  12. Thierry Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184-191, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.015.
  13. Thierry Coquand, Simon Huber, and Christian Sattler. Canonicity and homotopy canonicity for cubical type theory, 2021. URL: https://arxiv.org/abs/1902.06572.
  14. Thierry Coquand, Simon Huber, and Christian Sattler. Canonicity and homotopy canonicity for cubical type theory. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/lmcs-18(1:28)2022.
  15. Marcelo P. Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proceedings of the 4th international ACM SIGPLAN conference on Principles and practice of declarative programming, October 6-8, 2002, Pittsburgh, PA, USA (Affiliated with PLI 2002), pages 26-37. ACM, 2002. URL: https://doi.org/10.1145/571157.571161.
  16. Marcelo P. Fiore and Ola Mahmoud. Second-order algebraic theories. CoRR, abs/1308.5409, 2013. URL: https://arxiv.org/abs/1308.5409.
  17. Daniel Gratzer. Normalization for multimodal type theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3532398.
  18. Daniel Gratzer and Jonathan Sterling. Syntactic categories for dependent type theory: sketching and adequacy. CoRR, abs/2012.10783, 2020. URL: https://arxiv.org/abs/2012.10783.
  19. Robert Harper. An equational logical framework for type theories. CoRR, abs/2106.01484, 2021. URL: https://arxiv.org/abs/2106.01484.
  20. Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, 1993. URL: https://doi.org/10.1145/138027.138060.
  21. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  22. Martin Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 204-213. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782616.
  23. Jason Z. S. Hu, Brigitte Pientka, and Ulrich Schöpp. A category theoretic view of contextual types: from simple types to dependent types. CoRR, abs/2206.02831, 2022. URL: https://doi.org/10.48550/arXiv.2206.02831.
  24. Peter T Johnstone. Sketches of an elephant: a Topos theory compendium. Oxford logic guides. Oxford Univ. Press, New York, NY, 2002. URL: https://cds.cern.ch/record/592033.
  25. Achim Jung and Jerzy Tiuryn. A new characterization of lambda definability. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 245-257. Springer, 1993. URL: https://doi.org/10.1007/BFb0037110.
  26. Ambrus Kaposi. Type theory in a type theory with quotient inductive types. PhD thesis, University of Nottingham, UK, 2017. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.713896.
  27. Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for type theory. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 25:1-25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.25.
  28. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The homotopy theory of type theories. Advances in Mathematics, 337:1-38, 2018. URL: https://doi.org/10.1016/j.aim.2018.08.003.
  29. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In Harald Ganzinger, editor, Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, volume 1632 of Lecture Notes in Computer Science, pages 202-206. Springer, 1999. URL: https://doi.org/10.1007/3-540-48660-7_14.
  30. Loïc Pujet and Nicolas Tabareau. Impredicative Observational Equality. In POPL 2023 - 50th ACM SIGPLAN Symposium on Principles of Programming Languages, volume 7 of Proceedings of the ACM on programming languages, page 74, Boston, United States, January 2023. URL: https://doi.org/10.1145/3571739.
  31. Michael Shulman. Towards a third-generation HOTT. Talk series at the Homotopy Type Theory at CMU seminar, 2022. Google Scholar
  32. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, 2021. Version 1.1, revised May 2022. URL: https://doi.org/10.5281/zenodo.6990769.
  33. Jonathan Sterling. Naïve logical relations in synthetic Tait computability. Unpublished manuscript, June 2022. Google Scholar
  34. Jonathan Sterling and Carlo Angiuli. Normalization for cubical type theory. CoRR, abs/2101.11479, 2021. URL: https://arxiv.org/abs/2101.11479.
  35. Jonathan Sterling and Bas Spitters. Normalization by gluing for free λ-theories. CoRR, abs/1809.08646, 2018. URL: https://arxiv.org/abs/1809.08646.
  36. Taichi Uemura. A general framework for the semantics of type theory. CoRR, abs/1904.04097, 2019. URL: https://arxiv.org/abs/1904.04097.
  37. Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz, and Paige North. Synthetic Tait computability for simplicial type theory. In 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2022. URL: https://types22.inria.fr/files/2022/06/TYPES_2022_paper_17.pdf.
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 Imprint Privacy Contact