Document Open Access Logo

Gluing for Type Theory

Authors Ambrus Kaposi , Simon Huber, Christian Sattler

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.25.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
Simon Huber
  • University of Gothenburg, Sweden
Christian Sattler
  • University of Gothenburg, Sweden

Funding

  • Kaposi, Ambrus: The author was supported by the European Union, co-financed by the European Social Fund (EFOP-3.6.2-16-2017-00013, Thematic Fundamental Research Collaborations Grounding Innovation in Informatics and Infocommunications) and COST Action EUTypes CA15123.
  • Huber, Simon: I acknowledge the support of the Centre for Advanced Study (CAS) in Oslo, Norway, which funded and hosted the research project Homotopy Type Theory and Univalent Foundations during the academic year 2018/19.

Acknowledgements

The authors thank Thorsten Altenkirch, Simon Boulier, Thierry Coquand, András Kovács and Nicolas Tabareau for discussions related to the topics of this paper.

Cite AsGet BibTex

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.25

Abstract

The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Martin-Löf type theory
  • logical relations
  • parametricity
  • canonicity
  • quotient inductive types

Metrics

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

References

  1. Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. PACMPL, 2:23:1-23:29, 2017. Google Scholar
  2. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for system F. Unpublished draft, 1997. Google Scholar
  3. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodik and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837638.
  4. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science, Volume 13, Issue 4, October 2017. URL: http://dx.doi.org/10.23638/LMCS-13(4:1)2017.
  5. Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier. Theorie de Topos et Cohomologie Etale des Schemas I, volume 269 of Lecture Notes in Mathematics. Springer, 1971. Google Scholar
  6. Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 503-516. ACM, 2014. URL: http://dx.doi.org/10.1145/2535838.2535852.
  7. 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: http://dx.doi.org/10.1017/S0956796812000056.
  8. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. Google Scholar
  9. Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Mathematical Structures in Computer Science, 24(6), 2014. Google Scholar
  10. Thierry Coquand. Canonicity and normalisation for Dependent Type Theory. CoRR, abs/1810.09367, 2018. URL: http://arxiv.org/abs/1810.09367.
  11. Roy L. Crole. Categories for types. Cambridge mathematical textbooks. Cambridge University Press, Cambridge, New York, 1993. URL: http://opac.inria.fr/record=b1088776.
  12. Peter Dybjer. Internal Type Theory. In Lecture Notes in Computer Science, pages 120-134. Springer, 1996. Google Scholar
  13. Marcelo Fiore and Alex Simpson. Lambda Definability with Sums via Grothendieck Logical Relations. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, pages 147-161, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  14. 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: http://dx.doi.org/10.1145/571157.571161.
  15. Claudio Hermida, Uday S. Reddy, and Edmund P. Robinson. Logical Relations and Parametricity -– A Reynolds Programme for Category Theory and Programming Languages. Electronic Notes in Theoretical Computer Science, 303(0):149-180, 2014. Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013). URL: http://dx.doi.org/10.1016/j.entcs.2014.02.008.
  16. Martin Hofmann. Conservativity of Equality Reflection over Intensional Type Theory. In TYPES 95, pages 153-164, 1995. Google Scholar
  17. B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  18. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing Quotient Inductive-inductive Types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, January 2019. URL: http://dx.doi.org/10.1145/3290315.
  19. Chung kil Hur and Derek Dreyer. A Kripke logical relation between ML and assembly. Conference Record of the Annual ACM Symposium on Principles of Programming Languages, pages 133-146, January 2010. URL: http://dx.doi.org/10.1145/1926385.1926402.
  20. András Kovács. Formalisation of canonicity for type theory in Agda, November 2018. URL: https://github.com/AndrasKovacs/glue.
  21. J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge University Press, New York, NY, USA, 1986. Google Scholar
  22. Gordon D. Plotkin. Lambda-Definability and Logical Relations. Memorandum SAI-RM-4, University of Edinburgh, Edinburgh, Scotland, October 1973. Google Scholar
  23. Florian Rabe and Kristina Sojakova. Logical Relations for a Logical Framework. ACM Trans. Comput. Logic, 14(4):32:1-32:34, November 2013. URL: http://dx.doi.org/10.1145/2536740.2536741.
  24. John C. Reynolds. Types, Abstraction and Parametric Polymorphism. In R. E. A. Mason, editor, Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, September 19-23, 1983, pages 513-523. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1983. Google Scholar
  25. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25:1203-1277, June 2015. arXiv:1203.3253. URL: http://dx.doi.org/10.1017/S0960129514000565.
  26. Jonathan Sterling and Bas Spitters. Normalization by gluing for free λ-theories. CoRR, abs/1809.08646, 2018. URL: http://arxiv.org/abs/1809.08646.
  27. Andrew W. Appel and David Mcallester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23:657-683, September 2001. URL: http://dx.doi.org/10.1145/504709.504712.
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