ITU

What makes guarded types tick?

Research output: Contribution to conference - NOT published in proceeding or journalPaperResearchpeer-review

Standard

What makes guarded types tick? / Bahr, Patrick; Mannaa, Bassel; Møgelberg, Rasmus Ejlers.

2018. Paper presented at Programming And Reasoning on Infinite Structures, Oxford, United Kingdom.

Research output: Contribution to conference - NOT published in proceeding or journalPaperResearchpeer-review

Harvard

Bahr, P, Mannaa, B & Møgelberg, RE 2018, 'What makes guarded types tick?', Paper presented at Programming And Reasoning on Infinite Structures, Oxford, United Kingdom, 07/07/2018 - 08/07/2018.

APA

Bahr, P., Mannaa, B., & Møgelberg, R. E. (2018). What makes guarded types tick?. Paper presented at Programming And Reasoning on Infinite Structures, Oxford, United Kingdom.

Vancouver

Bahr P, Mannaa B, Møgelberg RE. What makes guarded types tick?. 2018. Paper presented at Programming And Reasoning on Infinite Structures, Oxford, United Kingdom.

Author

Bahr, Patrick ; Mannaa, Bassel ; Møgelberg, Rasmus Ejlers. / What makes guarded types tick?. Paper presented at Programming And Reasoning on Infinite Structures, Oxford, United Kingdom.

Bibtex

@conference{124396998505496e8aaf73590fe86131,
title = "What makes guarded types tick?",
abstract = "We give an overview of the syntax and semantics of Clocked Type Theory (CloTT), a dependent type theory for guarded recursion with many clocks, in which one can encode coinductive types and capture the notion of productivity in types. The main novelty of CloTT is the notion of ticks, which allows one to open the delay type modality, and, e.g., define a dependent form of applicative functor action, which can be used for reasoning about coinductive data. In the talk we will give examples of programming and reasoning about guarded recursive and coinductive data in CloTT, and we will present the main syntactic results: Strong normalisation, canonicity and decidability of type checking. If time permits, we will also sketch the main ideas of the denotational semantics for CloTT.",
author = "Patrick Bahr and Bassel Mannaa and M{\o}gelberg, {Rasmus Ejlers}",
year = "2018",
language = "English",
note = "Programming And Reasoning on Infinite Structures, PARIS 2018 ; Conference date: 07-07-2018 Through 08-07-2018",

}

RIS

TY - CONF

T1 - What makes guarded types tick?

AU - Bahr, Patrick

AU - Mannaa, Bassel

AU - Møgelberg, Rasmus Ejlers

PY - 2018

Y1 - 2018

N2 - We give an overview of the syntax and semantics of Clocked Type Theory (CloTT), a dependent type theory for guarded recursion with many clocks, in which one can encode coinductive types and capture the notion of productivity in types. The main novelty of CloTT is the notion of ticks, which allows one to open the delay type modality, and, e.g., define a dependent form of applicative functor action, which can be used for reasoning about coinductive data. In the talk we will give examples of programming and reasoning about guarded recursive and coinductive data in CloTT, and we will present the main syntactic results: Strong normalisation, canonicity and decidability of type checking. If time permits, we will also sketch the main ideas of the denotational semantics for CloTT.

AB - We give an overview of the syntax and semantics of Clocked Type Theory (CloTT), a dependent type theory for guarded recursion with many clocks, in which one can encode coinductive types and capture the notion of productivity in types. The main novelty of CloTT is the notion of ticks, which allows one to open the delay type modality, and, e.g., define a dependent form of applicative functor action, which can be used for reasoning about coinductive data. In the talk we will give examples of programming and reasoning about guarded recursive and coinductive data in CloTT, and we will present the main syntactic results: Strong normalisation, canonicity and decidability of type checking. If time permits, we will also sketch the main ideas of the denotational semantics for CloTT.

M3 - Paper

T2 - Programming And Reasoning on Infinite Structures

Y2 - 7 July 2018 through 8 July 2018

ER -

ID: 83193671