ITU

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

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

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 chapterArticle in proceedingsResearchpeer-review

Harvard

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

APA

Mannaa, B., & Møgelberg, R. E. (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 https://doi.org/10.4230/LIPIcs.FSCD.2018.23

Vancouver

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). https://doi.org/10.4230/LIPIcs.FSCD.2018.23

Author

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

Bibtex

@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.",
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/",

}

RIS

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.

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 -

ID: 83273856