Skip to Main content Skip to Navigation
Conference papers

Engineering Proof by Reflection in Agda

Abstract : This paper explores the recent addition to Agda enabling reflection, in the style of Lisp and Template Haskell. It gives a brief introduction to using reflection, and details the complexities encountered when automating certain proofs with proof by reflection. It presents a library that can be used for automatically quoting a class of concrete Agda terms to a non-dependent, user-defined inductive data type, alleviating some of the burden a programmer faces when using reflection in a practical setting.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Paul van der Walt Connect in order to contact the contributor
Submitted on : Tuesday, May 6, 2014 - 3:08:05 PM
Last modification on : Tuesday, August 13, 2019 - 10:16:03 AM
Long-term archiving on: : Wednesday, August 6, 2014 - 1:05:36 PM


Files produced by the author(s)



Paul van der Walt, Wouter Swierstra. Engineering Proof by Reflection in Agda. IFL - 24th International Symposium on Implementation and Application of Functional Languages, Aug 2012, Oxford, United Kingdom. pp.157-173, ⟨10.1007/978-3-642-41582-1_10⟩. ⟨hal-00987610⟩



Les métriques sont temporairement indisponibles