Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to e...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6278/pdf |
| _version_ | 1797268580668014592 |
|---|---|
| author | Bassel Mannaa Rasmus Ejlers Møgelberg Niccolò Veltri |
| author_facet | Bassel Mannaa Rasmus Ejlers Møgelberg Niccolò Veltri |
| author_sort | Bassel Mannaa |
| collection | DOAJ |
| description | Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for
programming with coinductive types, allowing productivity to be encoded in
types, and for reasoning about advanced programming language features using an
abstract form of step-indexing. CloTT has previously been shown to enjoy a
number of syntactic properties including strong normalisation, canonicity and
decidability of the equational theory. In this paper we present a denotational
semantics for CloTT useful, e.g., for studying future extensions of CloTT with
constructions such as path types.
The main challenge for constructing this model is to model the notion of
ticks on a clock used in CloTT for coinductive reasoning about coinductive
types. We build on a category previously used to model guarded recursion with
multiple clocks. In this category there is an object of clocks but no object of
ticks, and so tick-assumptions in a context can not be modelled using standard
tools. Instead we model ticks using dependent right adjoint functors, a
generalisation of the category theoretic notion of adjunction to the setting of
categories with families. Dependent right adjoints are known to model
Fitch-style modal types, but in the case of CloTT, the modal operators
constitute a family indexed internally in the type theory by clocks. We model
this family using a dependent right adjoint on the slice category over the
object of clocks. Finally we show how to model the tick constant of CloTT using
a semantic substitution.
This work improves on a previous model by the first two named authors which
not only had a flaw but was also considerably more complicated. |
| first_indexed | 2024-04-25T01:34:45Z |
| format | Article |
| id | doaj.art-a9a7e1a274d04aefbeb9d0be60936b9a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:45Z |
| publishDate | 2020-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-a9a7e1a274d04aefbeb9d0be60936b9a2024-03-08T10:32:05ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-12-01Volume 16, Issue 410.23638/LMCS-16(4:17)20206278Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theoryBassel MannaaRasmus Ejlers MøgelbergNiccolò VeltriClocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of the equational theory. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types. The main challenge for constructing this model is to model the notion of ticks on a clock used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion with multiple clocks. In this category there is an object of clocks but no object of ticks, and so tick-assumptions in a context can not be modelled using standard tools. Instead we model ticks using dependent right adjoint functors, a generalisation of the category theoretic notion of adjunction to the setting of categories with families. Dependent right adjoints are known to model Fitch-style modal types, but in the case of CloTT, the modal operators constitute a family indexed internally in the type theory by clocks. We model this family using a dependent right adjoint on the slice category over the object of clocks. Finally we show how to model the tick constant of CloTT using a semantic substitution. This work improves on a previous model by the first two named authors which not only had a flaw but was also considerably more complicated.https://lmcs.episciences.org/6278/pdfcomputer science - logic in computer science |
| spellingShingle | Bassel Mannaa Rasmus Ejlers Møgelberg Niccolò Veltri Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory Logical Methods in Computer Science computer science - logic in computer science |
| title | Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory |
| title_full | Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory |
| title_fullStr | Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory |
| title_full_unstemmed | Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory |
| title_short | Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory |
| title_sort | ticking clocks as dependent right adjoints denotational semantics for clocked type theory |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/6278/pdf |
| work_keys_str_mv | AT basselmannaa tickingclocksasdependentrightadjointsdenotationalsemanticsforclockedtypetheory AT rasmusejlersmøgelberg tickingclocksasdependentrightadjointsdenotationalsemanticsforclockedtypetheory AT niccoloveltri tickingclocksasdependentrightadjointsdenotationalsemanticsforclockedtypetheory |