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 realizers in our construction. NBE for simple types is u...
| Main Authors: | , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/34287/ |