The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review

Abstract

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 type checking. 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 used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion, but in this category there is no object of ticks, so tick-assumptions in a context can not be modelled using standard tools. Instead we show how ticks can be modelled using adjoint functors, and how to model the tick constant using a semantic substitution.
OriginalsprogEngelsk
Titel3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Antal sider17
Vol/bind108
ForlagSchloss Dagstuhl--Leibniz-Zentrum für Informatik
Publikationsdato2018
Artikelnummer23
ISBN (Trykt)978-3-95977-077-4
DOI
StatusUdgivet - 2018
BegivenhedInternational Conference on Formal Structures for Computation and Deduction - Oxford, Storbritannien
Varighed: 9 jul. 201812 jul. 2018
Konferencens nummer: 3
http://www.cs.le.ac.uk/events/fscd2018/

Konference

KonferenceInternational Conference on Formal Structures for Computation and Deduction
Nummer3
Land/OmrådeStorbritannien
ByOxford
Periode09/07/201812/07/2018
Internetadresse
NavnLeibniz International Proceedings in Informatics (LIPIcs)
Vol/bind108
ISSN1868-8969

Emneord

  • Clocked Type Theory
  • Guarded Recursion
  • Coinductive Types
  • Denotational Semantics
  • Step-Indexing

Fingeraftryk

Dyk ned i forskningsemnerne om 'The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory'. Sammen danner de et unikt fingeraftryk.

Citationsformater