Normalisation by evaluation for dependent types
(2016)
Presentation / Conference Contribution
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.