Abstract
We describe a category-theoretic semantics for a simply typed variant of Cocon, a contextual modal type theory where the box modality mediates between the weak function space that is used to represent higher-order abstract syntax (HOAS) trees and the strong function space that describes (recursive) computations about them. What makes Cocon different from standard type theories is the presence of first-class contexts and contextual objects to describe syntax trees that are closed with respect to a given context of assumptions. Following M. Hofmann’s work, we use a presheaf model to characterise HOAS trees. Surprisingly, this model already provides the necessary structure to also model Cocon. In particular, we can capture the contextual objects of Cocon using a comonad \(\flat \) that restricts presheaves to their closed elements. This gives a simple semantic characterisation of the invariants of contextual types (e.g. substitution invariance) and identifies Cocon as a type-theoretic syntax of presheaf models. We express our category-theoretic constructions by using a modal internal type theory that is implemented in Agda-Flat.
Chapter PDF
Similar content being viewed by others
References
The Agda sources for this paper are available from: http://github.com/uelis/contextual.
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type and scope safe universe of syntaxes with binding: Their semantics and proofs. Proc. ACM Program. Lang., 2(ICFP):90:1–90:30, July 2018.
Benton, P.N., Bierman, G.M., de Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings. vol. 664, pp. 75–90. Springer (1993)
Andrew Barber and Gordon Plotkin. Dual intuitionistic linear logic. Technical Report, LFCS, University of Edinburgh, 1997.
John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209 – 243, 1986.
Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555–604, 2001.
Peter Dybjer. Internal type theory. In Types for Proofs and Programs (TYPES’95), pages 120–134, 1995.
M. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In Logic in Computer Science (LICS’99), pages 193–202. IEEE Press, 1999.
Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In Logic in Computer Science (LICS’99), pages 214–224. IEEE Press, 1999.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, January 1993.
Martin Hofmann. Syntax and Semantics of Dependent Types, page 79–130. Publications of the Newton Institute. Cambridge University Press, 1997.
Martin Hofmann. Semantical analysis of higher-order abstract syntax. In Logic in Computer Science (LICS’99), pages 204–213. IEEE Press, 1999.
Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on nominal algebras in HOAS. In International Colloquium on Automata, Languages and Programming (ICALP’01), LNCS 2076, pages 963–978. Springer, 2001.
Bart Jacobs. Comprehension categories and the semantics of type dependency. Theor. Comput. Sci., 107(2):169–207, 1993.
Kavvos, G.A.: Intensionality, intensional recursion, and the Gödel-Löb axiom. CoRR abs/1703.01288 (2017), http://arxiv.org/abs/1703.01288
Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal universes in models of homotopy type theory. In Formal Structures for Computation and Deduction (FSCD’18), pages 22:1–22:17, 2018.
Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. ACM Comput. Surv., 31(3es), 1999.
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1–49, 2008.
Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Symposium on Language Design and Implementation (PLDI’88), pages 199–208, June 1988.
Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In Principles of Programming Languages (POPL’08), pages 371–382. ACM Press, 2008.
Brigitte Pientka and Andreas Abel. Well-founded recursion over contextual objects. In Typed Lambda Calculi and Applications (TLCA’15), pages 273–287, 2015.
Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and Rébecca Zucchini. Cocon: Computation in contextual type theory. CoRR, abs/1901.03378, 2019.
Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and Rebecca Zucchini. A type theory for defining logics and proofs. In 34th IEEE/ ACM Symposium on Logic in Computer Science (LICS’19), pages 1–13, IEEE Computer Society, 2019.
Brigitte Pientka and Andrew Cave. Inductive Beluga: Programming Proofs (System Description). In Conference on Automated Deduction (CADE-25), LNCS 9195, pages 272–281. Springer, 2015.
Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In Principles and Practice of Declarative Programming (PPDP’08), pages 163–173, 2008.
Brigitte Pientka and Joshua Dunfield. Beluga: a framework for programming and reasoning with deductive systems (System Description). In International Joint Conference on Automated Reasoning (IJCAR’10), LNAI 6173, pages 15–21. Springer, 2010.
Shulman, M.: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science 28(6), 856–941 (2018)
Thomas Streicher. Semantics of Type Theory. Birkhäuser, 1991.
Andrea Vezzosi. Agda with a flat modality. Available from https://github.com/agda/agda/tree/flat, 2018.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Pientka, B., Schöpp, U. (2020). Semantical Analysis of Contextual Types. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)