41 Search Results for "Coquand, Thierry"


Document
A General Constructive Form of Higman’s Lemma

Authors: Stefano Berardi, Gabriele Buriola, and Peter Schuster

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)


Abstract
In logic and computer science one often needs to constructivize a theorem ∀ f ∃ g.P(f,g), stating that for every infinite sequence f there is an infinite sequence g such that P(f,g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of ∀ f ∃ g.P(f,g): for every f there is a "long enough" finite prefix g₀ of g such that P(f,g₀), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version. Our approach with bars generalises the approaches to Higman’s lemma undertaken by Coquand-Fridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman’s lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman’s lemma, our constructive proofs are closer to the original classical proofs.

Cite as

Stefano Berardi, Gabriele Buriola, and Peter Schuster. A General Constructive Form of Higman’s Lemma. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{berardi_et_al:LIPIcs.CSL.2024.16,
  author =	{Berardi, Stefano and Buriola, Gabriele and Schuster, Peter},
  title =	{{A General Constructive Form of Higman’s Lemma}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{16:1--16:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.16},
  URN =		{urn:nbn:de:0030-drops-196599},
  doi =		{10.4230/LIPIcs.CSL.2024.16},
  annote =	{Keywords: intuitionistic logic, constructive mathematics, formal proof, inductive predicate, bar induction, well quasi-order, Higman’s lemma}
}
Document
Type Theory with Explicit Universe Polymorphism

Authors: Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)


Abstract
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system where we also have products indexed by universe levels and by constraints. Our theory has judgments for internal universe levels, built up from level variables by a successor operation and a binary supremum operation, and also judgments for equality of universe levels.

Cite as

Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Type Theory with Explicit Universe Polymorphism. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2022.13,
  author =	{Bezem, Marc and Coquand, Thierry and Dybjer, Peter and Escard\'{o}, Mart{\'\i}n},
  title =	{{Type Theory with Explicit Universe Polymorphism}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.13},
  URN =		{urn:nbn:de:0030-drops-184564},
  doi =		{10.4230/LIPIcs.TYPES.2022.13},
  annote =	{Keywords: type theory, universes in type theory, universe polymorphism, level-indexed products, constraint-indexed products}
}
Document
A Univalent Formalization of Constructive Affine Schemes

Authors: Max Zeuner and Anders Mörtberg

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)


Abstract
We present a formalization of constructive affine schemes in the Cubical Agda proof assistant. This development is not only fully constructive and predicative, it also makes crucial use of univalence. By now schemes have been formalized in various proof assistants. However, most existing formalizations follow the inherently non-constructive approach of Hartshorne’s classic "Algebraic Geometry" textbook, for which the construction of the so-called structure sheaf is rather straightforwardly formalizable and works the same with or without univalence. We follow an alternative approach that uses a point-free description of the constructive counterpart of the Zariski spectrum called the Zariski lattice and proceeds by defining the structure sheaf on formal basic opens and then lift it to the whole lattice. This general strategy is used in a plethora of textbooks, but formalizing it has proved tricky. The main result of this paper is that with the help of the univalence principle we can make this "lift from basis" strategy formal and obtain a fully formalized account of constructive affine schemes.

Cite as

Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 14:1-14:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
  author =	{Zeuner, Max and M\"{o}rtberg, Anders},
  title =	{{A Univalent Formalization of Constructive Affine Schemes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{14:1--14:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.14},
  URN =		{urn:nbn:de:0030-drops-184574},
  doi =		{10.4230/LIPIcs.TYPES.2022.14},
  annote =	{Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
Document
Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses

Authors: Taichi Uemura

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)


Abstract
We show that certain diagrams of ∞-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single ∞-logos but also a diagram of ∞-logoses. This also provides a higher dimensional version of Sterling’s synthetic Tait computability - a type theory for higher dimensional logical relations.

Cite as

Taichi Uemura. Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{uemura:LIPIcs.FSCD.2023.5,
  author =	{Uemura, Taichi},
  title =	{{Homotopy Type Theory as Internal Languages of Diagrams of ∞-Logoses}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.5},
  URN =		{urn:nbn:de:0030-drops-179897},
  doi =		{10.4230/LIPIcs.FSCD.2023.5},
  annote =	{Keywords: Homotopy type theory, ∞-logos, ∞-topos, oplax limit, Artin gluing, modality, synthetic Tait computability, logical relation}
}
Document
Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)

Authors: Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster

Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)


Abstract
At least from a practical and contemporary angle, the time-honoured question about the extent of intuitionistic mathematics rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. All this is ideally done by manipulating proofs mechanically or by adequate metatheorems, which includes proof translations, automated theorem proving, program extraction from proofs, proof analysis and proof mining. The question should thus be put as: What is the computational content of proofs? Guided by this central question, the present Dagstuhl seminar puts a special focus on coherent and geometric theories and their generalisations. These are not only widespread in mathematics and non-classical logics such as temporal and modal logics, but also a priori amenable for constructivisation, e.g., by Barr’s Theorem, and last but not least particularly suited as a basis for automated theorem proving. Specific topics include categorical semantics for geometric theories, complexity issues of and algorithms for geometrisation of theories including speed-up questions, the use of geometric theories in constructive mathematics including finding algorithms, proof-theoretic presentation of sheaf models and higher toposes, and coherent logic for automatically readable proofs.

Cite as

Thierry Coquand, Hajime Ishihara, Sara Negri, and Peter M. Schuster. Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472). In Dagstuhl Reports, Volume 11, Issue 10, pp. 151-172, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{coquand_et_al:DagRep.11.10.151,
  author =	{Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
  title =	{{Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472)}},
  pages =	{151--172},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{10},
  editor =	{Coquand, Thierry and Ishihara, Hajime and Negri, Sara and Schuster, Peter M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.11.10.151},
  URN =		{urn:nbn:de:0030-drops-159321},
  doi =		{10.4230/DagRep.11.10.151},
  annote =	{Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}
Document
Unifying Cubical Models of Univalent Type Theory

Authors: Evan Cavallo, Anders Mörtberg, and Andrew W Swan

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)


Abstract
We present a new constructive model of univalent type theory based on cubical sets. Unlike prior work on cubical models, ours depends neither on diagonal cofibrations nor connections. This is made possible by weakening the notion of fibration from the cartesian cubical set model, so that it is not necessary to assume that the diagonal on the interval is a cofibration. We have formally verified in Agda that these fibrations are closed under the type formers of cubical type theory and that the model satisfies the univalence axiom. By applying the construction in the presence of diagonal cofibrations or connections and reversals, we recover the existing cartesian and De Morgan cubical set models as special cases. Generalizing earlier work of Sattler for cubical sets with connections, we also obtain a Quillen model structure.

Cite as

Evan Cavallo, Anders Mörtberg, and Andrew W Swan. Unifying Cubical Models of Univalent Type Theory. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cavallo_et_al:LIPIcs.CSL.2020.14,
  author =	{Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W},
  title =	{{Unifying Cubical Models of Univalent Type Theory}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.14},
  URN =		{urn:nbn:de:0030-drops-116578},
  doi =		{10.4230/LIPIcs.CSL.2020.14},
  annote =	{Keywords: Cubical Set Models, Cubical Type Theory, Homotopy Type Theory, Univalent Foundations}
}
Document
Homotopy Canonicity for Cubical Type Theory

Authors: Thierry Coquand, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.

Cite as

Thierry Coquand, Simon Huber, and Christian Sattler. Homotopy Canonicity for Cubical Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.FSCD.2019.11,
  author =	{Coquand, Thierry and Huber, Simon and Sattler, Christian},
  title =	{{Homotopy Canonicity for Cubical Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{11:1--11:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.11},
  URN =		{urn:nbn:de:0030-drops-105188},
  doi =		{10.4230/LIPIcs.FSCD.2019.11},
  annote =	{Keywords: cubical type theory, univalence, canonicity, sconing, Artin glueing}
}
Document
Gluing for Type Theory

Authors: Ambrus Kaposi, Simon Huber, and Christian Sattler

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.

Cite as

Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{kaposi_et_al:LIPIcs.FSCD.2019.25,
  author =	{Kaposi, Ambrus and Huber, Simon and Sattler, Christian},
  title =	{{Gluing for Type Theory}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.25},
  URN =		{urn:nbn:de:0030-drops-105323},
  doi =		{10.4230/LIPIcs.FSCD.2019.25},
  annote =	{Keywords: Martin-L\"{o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
Document
Cubical Syntax for Reflection-Free Extensional Equality

Authors: Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false.

Cite as

Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. Cubical Syntax for Reflection-Free Extensional Equality. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 31:1-31:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{sterling_et_al:LIPIcs.FSCD.2019.31,
  author =	{Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  title =	{{Cubical Syntax for Reflection-Free Extensional Equality}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{31:1--31:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31},
  URN =		{urn:nbn:de:0030-drops-105387},
  doi =		{10.4230/LIPIcs.FSCD.2019.31},
  annote =	{Keywords: Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity}
}
Document
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic

Authors: Robin Adams, Marc Bezem, and Thierry Coquand

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)


Abstract
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity - that every closed term computes to a canonical form. A computation becomes "stuck" when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension. As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Omega. There are proofs which inhabit propositions, which are the terms of type Omega. The canonical propositions are those constructed from false by implication. Thirdly, there are paths which inhabit equations M =_A N, where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality - logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity. We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.

Cite as

Robin Adams, Marc Bezem, and Thierry Coquand. A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{adams_et_al:LIPIcs.TYPES.2016.3,
  author =	{Adams, Robin and Bezem, Marc and Coquand, Thierry},
  title =	{{A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.3},
  URN =		{urn:nbn:de:0030-drops-98581},
  doi =		{10.4230/LIPIcs.TYPES.2016.3},
  annote =	{Keywords: type theory, univalence, canonicity}
}
Document
Realizability at Work: Separating Two Constructive Notions of Finiteness

Authors: Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)


Abstract
We elaborate in detail a realizability model for Martin-Löf dependent type theory with the purpose to analyze a subtle distinction between two constructive notions of finiteness of a set A. The two notions are: (1) A is Noetherian: the empty list can be constructed from lists over A containing duplicates by a certain inductive shortening process; (2) A is streamless: every enumeration of A contains a duplicate.

Cite as

Marc Bezem, Thierry Coquand, Keiko Nakata, and Erik Parmann. Realizability at Work: Separating Two Constructive Notions of Finiteness. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TYPES.2016.6,
  author =	{Bezem, Marc and Coquand, Thierry and Nakata, Keiko and Parmann, Erik},
  title =	{{Realizability at Work: Separating Two Constructive Notions of Finiteness}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.6},
  URN =		{urn:nbn:de:0030-drops-98541},
  doi =		{10.4230/LIPIcs.TYPES.2016.6},
  annote =	{Keywords: Type theory, realizability, constructive notions of finiteness}
}
Document
Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

Authors: Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)


Abstract
This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

Cite as

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 5:1-5:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{cohen_et_al:LIPIcs.TYPES.2015.5,
  author =	{Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
  title =	{{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{5:1--5:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.5},
  URN =		{urn:nbn:de:0030-drops-84754},
  doi =		{10.4230/LIPIcs.TYPES.2015.5},
  annote =	{Keywords: univalence axiom, dependent type theory, cubical sets}
}
Document
The Ackermann Award 2016

Authors: Thierry Coquand and Anuj Dawar

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)


Abstract
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2016 edition of the award.

Cite as

Thierry Coquand and Anuj Dawar. The Ackermann Award 2016. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{coquand_et_al:LIPIcs.CSL.2016.1,
  author =	{Coquand, Thierry and Dawar, Anuj},
  title =	{{The Ackermann Award 2016}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{1:1--1:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.1},
  URN =		{urn:nbn:de:0030-drops-65419},
  doi =		{10.4230/LIPIcs.CSL.2016.1},
  annote =	{Keywords: Ackermann Award, Computer Science, Logic}
}
Document
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-dev.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}
}
Document
Non-Constructivity in Kan Simplicial Sets

Authors: Marc Bezem, Thierry Coquand, and Erik Parmann

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)


Abstract
We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y^X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.

Cite as

Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{bezem_et_al:LIPIcs.TLCA.2015.92,
  author =	{Bezem, Marc and Coquand, Thierry and Parmann, Erik},
  title =	{{Non-Constructivity in Kan Simplicial Sets}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{92--106},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.92},
  URN =		{urn:nbn:de:0030-drops-51579},
  doi =		{10.4230/LIPIcs.TLCA.2015.92},
  annote =	{Keywords: Constructive logic, simplicial sets, semantics of simple types}
}
  • Refine by Author
  • 15 Coquand, Thierry
  • 5 Bezem, Marc
  • 4 Huber, Simon
  • 4 Lombardi, Henri
  • 3 Mörtberg, Anders
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Type theory
  • 4 Theory of computation → Constructive mathematics
  • 3 Theory of computation → Proof theory
  • 2 Theory of computation → Denotational semantics
  • 1 Mathematics of computing → Discrete mathematics
  • Show More...

  • Refine by Keyword
  • 4 canonicity
  • 4 computer algebra
  • 3 Constructive Mathematics
  • 3 Kepler conjecture
  • 3 type theory
  • Show More...

  • Refine by Type
  • 41 document

  • Refine by Publication Year
  • 23 2006
  • 3 2018
  • 3 2019
  • 3 2023
  • 2 2016
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail