Authors: Pientka Brigitte, Schöpp Ulrich Published on:Publication:
Foundations of Software Science and Computation Structures;12077:50221 DOI: 10.1007/9783030452315_26
We describe a categorytheoretic 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 higherorder 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 firstclass 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 typetheoretic syntax of presheaf models. We express our categorytheoretic constructions by using a modal internal type theory that is implemented in AgdaFlat.
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.)