Normalisation by evaluation for type theory, in type theory
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every constru...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Logical Methods in Computer Science e.V.
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/47642/ |