DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2018.23

The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory

Authors: Bassel Mannaa and Rasmus Ejlers Møgelberg

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

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.

Cite as

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

Copy BibTex To Clipboard

@InProceedings{mannaa_et_al:LIPIcs.FSCD.2018.23,
  author =	{Mannaa, Bassel and M{\o}gelberg, Rasmus Ejlers},
  title =	{{The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.23},
  URN =		{urn:nbn:de:0030-drops-91938},
  doi =		{10.4230/LIPIcs.FSCD.2018.23},
  annote =	{Keywords: Guarded type theory, Coinduction, Presheaf model, Clocked type theory, Dependent adjunction}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2016.17

The Independence of Markov’s Principle in Type Theory

Authors: Thierry Coquand and Bassel Mannaa

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One tentative way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. It is however not clear how to interpret the universe in a sheaf model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.

Cite as

Thierry Coquand and Bassel Mannaa. The Independence of Markov’s Principle in Type Theory. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.FSCD.2016.17,
  author =	{Coquand, Thierry and Mannaa, Bassel},
  title =	{{The Independence of Markov’s Principle in Type Theory}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.17},
  URN =		{urn:nbn:de:0030-drops-59939},
  doi =		{10.4230/LIPIcs.FSCD.2016.17},
  annote =	{Keywords: Forcing, Dependent type theory, Markov's Principle, Cantor Space}
}

Search Results

Documents authored by Mannaa, Bassel

The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory

Abstract

Cite as

The Independence of Markov’s Principle in Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message