Engineering Proof by Reflection in Agda

By Paul van der Walt and Wouter Swierstra.
2012, 24th IFL, LNCS8241:157–173, Oxford. [pdf] [code]

Posted on 15 March, 2013.


Download full article here: pdf.

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.



paul (at) thisdomain
GPG: 0xEAF20AB71D1292C0