Document Open Access Logo

Encoding Agda Programs Using Rewriting

Author Guillaume Genestier

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2020.31.pdf
  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Type theory
Keywords
  • Logical Frameworks
  • Rewriting
  • Universe Polymorphism
  • Eta Conversion

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Guillaume Genestier. Encoding Agda Programs Using Rewriting. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.31

Author Details

Guillaume Genestier
  • Université Paris-Saclay, ENS Paris-Saclay, Inria, CNRS, LSV, France
  • MINES ParisTech, PSL University, France

Funding

Part of this work was carried out during a stay at Chalmers University of Technology, Sweden, funded by the Cost Action CA15123: EUTypes.

Acknowledgements

I am grateful to Jesper Cockx and Andreas Abel, who received me in Chalmers and helped me to find my way in the hostile jungle the Agda implementation would have been without their help. Then I would like to thank Frédéric Blanqui, Olivier Hermant, Kostia Chardonnet and the anonymous reviewers for their thorough comments, both on the form and content of this article, which greatly improved its quality.

Supplementary Materials

  • 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].

References

  1. Ali Assaf. https://pastel.archives-ouvertes.fr/tel-01235303v4. PhD thesis, École polytechnique, France, 2015. URL: https://pastel.archives-ouvertes.fr/tel-01235303v4.
  2. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a logical framework based on the λπ-calculus modulo theory, 2019. URL: http://www.lsv.fr/~dowek/Publi/expressing.pdf.
  3. Henk P. Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, Handbook of Logic in Computer Science (Vol. 2), pages 117-309. Oxford University Press, Inc., New York, NY, USA, 1992. Google Scholar
  4. Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. https://doi.org/10.1016/S0304-3975(00)00373-X. Theoretical Computer Science, 266(1-2):773-818, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00373-X.
  5. Stefano Berardi. http://www.di.unito.it/~stefano/Berardi-PhDThesis.rtf. Phd, Carnegie Mellon University, Dept. Comp. Sci., Pittsburgh, Pennsylvania, USA and Torino University, Dipartimento di Informatica, Torino, Italy, 1990. URL: http://www.di.unito.it/~stefano/Berardi-PhDThesis.rtf.
  6. Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. http://ceur-ws.org/Vol-878/paper2.pdf. PxTP, page 16, 2012. URL: http://ceur-ws.org/Vol-878/paper2.pdf.
  7. Jesper Cockx and Guillaume Genestier. Agda2dedukti. https://github.com/Deducteam/Agda2Dedukti, 2019. URL: https://github.com/Deducteam/Agda2Dedukti.
  8. Denis Cousineau and Gilles Dowek. http://doi.org/10.1007/978-3-540-73228-0_9. In Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 4583, 2007. URL: http://doi.org/10.1007/978-3-540-73228-0_9.
  9. Nils Anders Danielsson, Matthew Daggitt, and Guillaume Allais. Agda standard library. https://github.com/agda/agda-stdlib, 2010-. URL: https://github.com/agda/agda-stdlib.
  10. Deducteam. Dedukti. https://deducteam.github.io/, 2011-. URL: https://deducteam.github.io/.
  11. Gilles Dowek, Gérard Huet, and Benjamin Werner. https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.6346&rep=rep1&type=pdf. In Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 115-130, 1993. URL: https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.38.6346&rep=rep1&type=pdf.
  12. Herman Geuvers and Mark-Jan Nederhof. https://doi.org/10.1017/S0956796800020037. Journal of Functional Programming, 1(2):155–189, 1991. URL: https://doi.org/10.1017/S0956796800020037.
  13. Robert Harper, Furio Honsell, and Gordon Plotkin. http://portal.acm.org/citation.cfm?doid=138027.138060. Journal of the ACM, 40(1):143-184, January 1993. URL: http://portal.acm.org/citation.cfm?doid=138027.138060.
  14. Robert Harper and Randy Pollack. https://doi.org/10.1016/0304-3975(90)90108-T. Theoretical Computer Science, 89:107-136, 1991. URL: https://doi.org/10.1016/0304-3975(90)90108-T.
  15. Zhaohui Luo. Computation and reasoning - a type theory for computer science, volume 11 of International series of monographs on computer science. Oxford University Press, 1994. Google Scholar
  16. Dale Miller. https://doi.org/10.1093/logcom/1.4.497. J. Log. Comput., 1(4):497-536, 1991. URL: https://doi.org/10.1093/logcom/1.4.497.
  17. Ulf Norell. http://www.cse.chalmers.se/~ulfn/papers/thesis.html. Phd, Chalmers University of Technology, Gothenburg, Sweden, 2007. URL: http://www.cse.chalmers.se/~ulfn/papers/thesis.html.
  18. Ulf Norell, Andreas Abel, Niels Anders Danielsson, Makoto Takeyama, and Catarina Coquand. Agda. https://github.com/agda/agda, 2007-, v1.0 : 1999. URL: https://github.com/agda/agda.
  19. Matthieu Sozeau and Nicolas Tabareau. https://doi.org/10.1007/978-3-319-08970-6_32. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving, pages 499-514. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_32.
  20. François Thiré. https://doi.org/10.4204/EPTCS.274.5. In Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP, pages 57-71, 2018. URL: https://doi.org/10.4204/EPTCS.274.5.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact