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.
Type de document :
Communication dans un congrès
Ralf Hinze. IFL - 24th International Symposium on Implementation and Application of Functional Languages, Aug 2012, Oxford, United Kingdom. Springer, 8241, pp.157-173, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-41582-1_10〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00987610
Contributeur : Paul Van Der Walt <>
Soumis le : mardi 6 mai 2014 - 15:08:05
Dernière modification le : mardi 6 mai 2014 - 15:32:34
Document(s) archivé(s) le : mercredi 6 août 2014 - 13:05:36

Fichier

ReflectionProofs.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Paul Van Der Walt, Wouter Swierstra. Engineering Proof by Reflection in Agda. Ralf Hinze. IFL - 24th International Symposium on Implementation and Application of Functional Languages, Aug 2012, Oxford, United Kingdom. Springer, 8241, pp.157-173, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-41582-1_10〉. 〈hal-00987610〉

Partager

Métriques

Consultations de la notice

268

Téléchargements de fichiers

517