Authors: Pientka Brigitte, Schöpp Ulrich Published on:-Publication:
Foundations of Software Science and Computation Structures;12077:502-21 DOI: 10.1007/978-3-030-45231-5_26
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 \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\flat $$\end{document}♭ 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.
Article Analysis: --
No tags are applied.
No tags found.
Additional Information
Journal:
Journal Article
Source:
PMC: PMC7788623
issn_isbn:
-
Country:
-
Language:
eng
article_id: 563840
More Info | #563840: Semantical Analysis of Contextual Types.
View PDF / Links: (#563840Semantical Analysis of Contextual Types.)