License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.10
URN: urn:nbn:de:0030-drops-162917
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16291/
Go to the corresponding LIPIcs Volume Portal

Cohen, Liron ; Rahli, Vincent

Constructing Unprejudiced Extensional Type Theories with Choices via Modalities

pdf-format:
LIPIcs-FSCD-2022-10.pdf (1 MB)

Abstract

Time-progressing expressions, i.e., expressions that compute to different values over time such as Brouwerian choice sequences or reference cells, are a common feature in many frameworks. For type theories to support such elements, they usually employ sheaf models. In this paper, we provide a general framework in the form of an extensional type theory incorporating various time-progressing elements along with a general possible-worlds forcing interpretation parameterized by modalities. The modalities can, in turn, be instantiated with topological spaces of bars, leading to a general sheaf model. This parameterized construction allows us to capture a distinction between theories that are "agnostic", i.e., compatible with classical reasoning in the sense that classical axioms can be validated, and those that are "intuitionistic", i.e., incompatible with classical reasoning in the sense that classical axioms can be proven false. This distinction is made via properties of the modalities selected to model the theory and consequently via the space of bars instantiating the modalities. We further identify a class of time-progressing elements that allows deriving "intuitionistic" theories that include not only choice sequences but also simpler operators, namely reference cells.

BibTeX - Entry

@InProceedings{cohen_et_al:LIPIcs.FSCD.2022.10,
  author =	{Cohen, Liron and Rahli, Vincent},
  title =	{{Constructing Unprejudiced Extensional Type Theories with Choices via Modalities}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{10:1--10:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16291},
  URN =		{urn:nbn:de:0030-drops-162917},
  doi =		{10.4230/LIPIcs.FSCD.2022.10},
  annote =	{Keywords: Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Choice sequences, References, Classical Logic, Theorem proving, Agda}
}

Keywords: Intuitionism, Extensional Type Theory, Constructive Type Theory, Realizability, Choice sequences, References, Classical Logic, Theorem proving, Agda
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI