Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.31
URN: urn:nbn:de:0030-drops-123530
URL: https://drops.dagstuhl.de/opus/volltexte/2020/12353/
Genestier, Guillaume
Encoding Agda Programs Using Rewriting
| pdf-format: |
|
Abstract
We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [Harper et al., 1993] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.
BibTeX - Entry
@InProceedings{genestier:LIPIcs:2020:12353,
author = {Guillaume Genestier},
title = {{Encoding Agda Programs Using Rewriting}},
booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
pages = {31:1--31:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-155-9},
ISSN = {1868-8969},
year = {2020},
volume = {167},
editor = {Zena M. Ariola},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12353},
URN = {urn:nbn:de:0030-drops-123530},
doi = {10.4230/LIPIcs.FSCD.2020.31},
annote = {Keywords: Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion}
}
| Keywords: | Logical Frameworks, Rewriting, Universe Polymorphism, Eta Conversion | |
| Seminar: | 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) | |
| Issue date: | 2020 | |
| Date of publication: | 28.06.2020 | |
| Supplementary Material: | The translator is available at https://github.com/Deducteam/Agda2Dedukti, the directory theory/ contains the encoding presented in Sections 3 and 4. It is able to translate and type-check 162 files of Agda’s standard library [Danielsson et al., 2010]. |
