Search

• < Previous
• 1
• Next >

---

On Irrelevance and Algorithmic Equality in Predicative Type Theory

Andreas Abel ; Gabriel Scherer.

Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been put forward. We consider Pfenning's type theory with&nbsp;[&hellip;]

---

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;]

---

Semi-continuous Sized Types and Termination

Andreas Abel.

Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound if&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;]

---