All Outputs (3)

Extending Homotopy Type Theory with Strict Equality (2016)
Conference Proceeding
Altenkirch, T., Capriotti, P., & Kraus, N. (2016). Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (21:1-21:17). https://doi.org/10.4230/LIPIcs.CSL.2016.21

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)
Conference Proceeding
Altenkirch, T., & Kaposi, A. (2016). Normalisation by evaluation for dependent types.

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)
Conference Proceeding
Altenkirch, T., & Kaposi, A. (2016). Type theory in type theory using quotient inductive types. In POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (18-29). https://doi.org/10.1145/2837614.2837638

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.