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/ |
| _version_ | 1848797595760066560 |
|---|---|
| author | Altenkirch, Thorsten Kaposi, Ambrus |
| author_facet | Altenkirch, Thorsten Kaposi, Ambrus |
| author_sort | Altenkirch, Thorsten |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | 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 construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda. |
| first_indexed | 2025-11-14T20:06:23Z |
| format | Article |
| id | nottingham-47642 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T20:06:23Z |
| publishDate | 2017 |
| publisher | Logical Methods in Computer Science e.V. |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-476422020-05-04T19:13:26Z https://eprints.nottingham.ac.uk/47642/ Normalisation by evaluation for type theory, in type theory Altenkirch, Thorsten Kaposi, Ambrus 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 construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda. Logical Methods in Computer Science e.V. 2017-10-23 Article PeerReviewed Altenkirch, Thorsten and Kaposi, Ambrus (2017) Normalisation by evaluation for type theory, in type theory. Logical Methods in Computer Science, 13 (4:1). pp. 1-26. ISSN 1860-5974 normalisation by evaluation; dependent types; internal type theory; logical relations; Agda https://lmcs.episciences.org/4005 doi:10.23638/LMCS-13(4:1)2017 doi:10.23638/LMCS-13(4:1)2017 |
| spellingShingle | normalisation by evaluation; dependent types; internal type theory; logical relations; Agda Altenkirch, Thorsten Kaposi, Ambrus Normalisation by evaluation for type theory, in type theory |
| title | Normalisation by evaluation for type theory, in type theory |
| title_full | Normalisation by evaluation for type theory, in type theory |
| title_fullStr | Normalisation by evaluation for type theory, in type theory |
| title_full_unstemmed | Normalisation by evaluation for type theory, in type theory |
| title_short | Normalisation by evaluation for type theory, in type theory |
| title_sort | normalisation by evaluation for type theory, in type theory |
| topic | normalisation by evaluation; dependent types; internal type theory; logical relations; Agda |
| url | https://eprints.nottingham.ac.uk/47642/ https://eprints.nottingham.ac.uk/47642/ https://eprints.nottingham.ac.uk/47642/ |