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/ |
| _version_ | 1848794816990674944 |
|---|---|
| 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 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 using 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 have formalized parts of the construction in Agda. |
| first_indexed | 2025-11-14T19:22:13Z |
| format | Conference or Workshop Item |
| id | nottingham-34287 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T19:22:13Z |
| publishDate | 2016 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-342872020-05-04T17:55:07Z https://eprints.nottingham.ac.uk/34287/ Normalisation by evaluation for dependent types Altenkirch, Thorsten Kaposi, Ambrus 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 using 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 have formalized parts of the construction in Agda. 2016-06-26 Conference or Workshop Item PeerReviewed Altenkirch, Thorsten and Kaposi, Ambrus (2016) Normalisation by evaluation for dependent types. In: FSCD 2016: 1st International Conference on Formal Structures for Computation and Deduction, 22-26 June 2016, Porto, Portugal. Normalisation by evaluation dependent types internal type theory logical relations Agda http://drops.dagstuhl.de/opus/volltexte/2016/5972/pdf/LIPIcs-FSCD-2016-6.pdf |
| spellingShingle | Normalisation by evaluation dependent types internal type theory logical relations Agda Altenkirch, Thorsten Kaposi, Ambrus Normalisation by evaluation for dependent types |
| title | Normalisation by evaluation for dependent types |
| title_full | Normalisation by evaluation for dependent types |
| title_fullStr | Normalisation by evaluation for dependent types |
| title_full_unstemmed | Normalisation by evaluation for dependent types |
| title_short | Normalisation by evaluation for dependent types |
| title_sort | normalisation by evaluation for dependent types |
| topic | Normalisation by evaluation dependent types internal type theory logical relations Agda |
| url | https://eprints.nottingham.ac.uk/34287/ https://eprints.nottingham.ac.uk/34287/ |