@inproceedings{fossacs20, author = {Pientka, Brigitte and Sch{\"{o}}pp, Ulrich}, title = {Semantical Analysis of Contextual Types}, booktitle = {Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {12077}, pages = {502--521}, year = {2020}, month = apr, 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 ♭ 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.}, isbn = {978-3-030-45231-5}, doi = {10.1007/978-3-030-45231-5_26}, }