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

Bassel Mannaa; Rasmus Ejlers Møgelberg

doi:10.4230/LIPIcs.FSCD.2018.23

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

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-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.

Original language	English
Title of host publication	3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Number of pages	17
Volume	108
Publisher	Schloss Dagstuhl--Leibniz-Zentrum für Informatik
Publication date	2018
Article number	23
ISBN (Print)	978-3-95977-077-4
DOIs	https://doi.org/10.4230/LIPIcs.FSCD.2018.23
Publication status	Published - 2018
Event	International Conference on Formal Structures for Computation and Deduction - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018 Conference number: 3 http://www.cs.le.ac.uk/events/fscd2018/

Conference

Conference	International Conference on Formal Structures for Computation and Deduction
Number	3
Country/Territory	United Kingdom
City	Oxford
Period	09/07/2018 → 12/07/2018
Internet address	http://www.cs.le.ac.uk/events/fscd2018/

Series	Leibniz International Proceedings in Informatics (LIPIcs)
Volume	108
ISSN	1868-8969

Keywords

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

Access to Document

10.4230/LIPIcs.FSCD.2018.23Licence: CC BY

TheClocksTheyAreAdjunctionsFinal published version, 518 KBLicence: CC BY

Type theories for reactive programming
Møgelberg, R. E. (PI), Vezzosi, A. (CoI), Graulund, C. U. (CoI), Kristensen, M. B. (CoI) & Veltri, N. (CoI)
Villum Foundation
22/01/2016 → 21/01/2022
Project: Research
Guarded recursive types in the foundations of programming
Møgelberg, R. E. (PI), Mannaa, B. (CoI) & Bahr, P. (CoI)
Independent Research Fund Denmark
01/07/2015 → 31/01/2019
Project: Research

Cite this

@inproceedings{1bed90c29f6d43dc837dd7687682859b,

title = "The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory",

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 semanticsfor 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.",

keywords = "Clocked Type Theory, Guarded Recursion, Coinductive Types, Denotational Semantics, Step-Indexing, Clocked Type Theory, Guarded Recursion, Coinductive Types, Denotational Semantics, Step-Indexing",

author = "Bassel Mannaa and M{\o}gelberg, {Rasmus Ejlers}",

year = "2018",

doi = "10.4230/LIPIcs.FSCD.2018.23",

language = "English",

isbn = "978-3-95977-077-4",

volume = "108",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik",

booktitle = "3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)",

note = "International Conference on Formal Structures for Computation and Deduction, FSCD 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

url = "http://www.cs.le.ac.uk/events/fscd2018/",

}

Mannaa, B & Møgelberg, RE 2018, The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory. in 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). vol. 108, 23, Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 108, International Conference on Formal Structures for Computation and Deduction, Oxford, United Kingdom, 09/07/2018. https://doi.org/10.4230/LIPIcs.FSCD.2018.23

The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory. / Mannaa, Bassel; Møgelberg, Rasmus Ejlers.
3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Vol. 108 Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2018. 23 (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

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

AU - Mannaa, Bassel

AU - Møgelberg, Rasmus Ejlers

N1 - Conference code: 3

PY - 2018

Y1 - 2018

N2 - 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 semanticsfor 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.

AB - 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 semanticsfor 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.

KW - Clocked Type Theory

KW - Guarded Recursion

KW - Coinductive Types

KW - Denotational Semantics

KW - Step-Indexing

KW - Clocked Type Theory

KW - Guarded Recursion

KW - Coinductive Types

KW - Denotational Semantics

KW - Step-Indexing

U2 - 10.4230/LIPIcs.FSCD.2018.23

DO - 10.4230/LIPIcs.FSCD.2018.23

M3 - Article in proceedings

SN - 978-3-95977-077-4

VL - 108

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

BT - 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

PB - Schloss Dagstuhl--Leibniz-Zentrum für Informatik

T2 - International Conference on Formal Structures for Computation and Deduction

Y2 - 9 July 2018 through 12 July 2018

ER -

Mannaa B, Møgelberg RE. The Clocks They Are Adjunctions: Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Vol. 108. Schloss Dagstuhl--Leibniz-Zentrum für Informatik. 2018. 23. (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108). doi: 10.4230/LIPIcs.FSCD.2018.23

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

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

Type theories for reactive programming

Guarded recursive types in the foundations of programming

Cite this