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 metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00987610
Contributor : Paul van der Walt <>
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

File

ReflectionProofs.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

333

Files downloads

1367