All Outputs (3)

Extending Homotopy Type Theory with Strict Equality (2016)
Presentation / Conference Contribution
Altenkirch, T., Capriotti, P., & Kraus, N. (2016, August). Extending Homotopy Type Theory with Strict Equality. Presented at 25th EACSL Annual Conference on Computer Science Logic, CSL 2016., Marseille, France

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult a... Read More about Extending Homotopy Type Theory with Strict Equality.

Normalisation by evaluation for dependent types (2016)
Presentation / Conference Contribution
Altenkirch, T., & Kaposi, A. Normalisation by evaluation for dependent types. Presented at FSCD 2016: 1st International Conference on Formal Structures for Computation and Deduction

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realiz... Read More about Normalisation by evaluation for dependent types.

Type theory in type theory using quotient inductive types (2016)
Presentation / Conference Contribution
Altenkirch, T., & Kaposi, A. (2016, January). Type theory in type theory using quotient inductive types. Presented at POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St Petersburg, Florida, USA

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids r... Read More about Type theory in type theory using quotient inductive types.