Search

• < Previous
• 1
• Next >

---

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

Andreas Abel ; Thierry Coquand ; Miguel Pagano.

We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation-by-evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type&nbsp;[&hellip;]

---

A proof of strong normalisation using domain theory

Thierry Coquand ; Arnaud Spiwack.

Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain&nbsp;[&hellip;]

---

Notions of Anonymous Existence in Martin-L\"of Type Theory

Nicolai Kraus ; Martín Escardó ; Thierry Coquand ; Thorsten Altenkirch.

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these&nbsp;[&hellip;]

---

The Independence of Markov's Principle in Type Theory

Thierry Coquand ; Bassel Mannaa.

In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One 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&nbsp;[&hellip;]

---

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

Andreas Abel ; Thierry Coquand.

Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F equipped with a decider for type equality. It refutes&nbsp;[&hellip;]

---

Canonicity and homotopy canonicity for cubical type theory

Thierry Coquand ; Simon Huber ; Christian Sattler.

Cubical type theory provides a constructive justification of homotopy type theory. 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. We present in this article two canonicity&nbsp;[&hellip;]

---

Reduction Free Normalisation for a proof irrelevant type of propositions

Thierry Coquand.

We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion&nbsp;[&hellip;]

---