Engineering Proof by Reflection in Agda - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

Engineering Proof by Reflection in Agda

Wouter Swierstra
  • Function : Author
  • PersonId : 955940


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.
Fichier principal
Vignette du fichier
ReflectionProofs.pdf (168.76 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00987610 , version 1 (06-05-2014)



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⟩
199 View
1914 Download



Gmail Facebook Twitter LinkedIn More