Advertisement

Engineering Proof by Reflection in Agda

  • Paul van der WaltEmail author
  • Wouter Swierstra
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8241)

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.

Keywords

Dependently-typed programming Reflection Agda Proof by reflection Metaprogramming 

Notes

Acknowledgements

We would like to thank each of the four anonymous reviewers for taking the time to provide detailed and constructive comments that greatly improved the article.

References

  1. 1.
    Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden (2007)Google Scholar
  2. 2.
    Norell, U.: Dependently typed programming in Agda. In: Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI ’09, pp. 1–2. ACM, New York (2009)Google Scholar
  3. 3.
    van der Walt, P.: Reflection in Agda. Master’s thesis, Department of Computer Science, Utrecht University, Utrecht, The Netherlands. http://igitur-archive.library.uu.nl/student-theses/2012-1030-200720/UUindex.html (2012)
  4. 4.
    Pitman, K.M.: Special forms in Lisp. In: Proceedings of the ACM Conference on LISP and Functional Programming, pp. 179–187. ACM (1980)Google Scholar
  5. 5.
    Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM ’97 (1997)Google Scholar
  6. 6.
    Sheard, T., Peyton Jones, S.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pp. 1–16 (2002)Google Scholar
  7. 7.
    Martin-Löf, P.: Constructive mathematics and computer programming. In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp. 167–184. Prentice-Hall Inc., Upper Saddle River (1985)Google Scholar
  8. 8.
    Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Oury, N., Swierstra, W.: The power of pi. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP ’08, pp. 39–50. ACM, New York (2008)CrossRefGoogle Scholar
  10. 10.
    Agda Developers: Agda release notes, regarding reflection. The Agda Wiki: http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-8 and http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-3-0 (2013). Accessed 9 Feb 2013
  11. 11.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Chlipala, A.: Certified Programming with Dependent Types. MIT Press, New York (2011)Google Scholar
  13. 13.
    Jedynak, W.: Agda ring solver using reflection. GitHub. https://github.com/wjzz/Agda-reflection-for-semiring-solver (2012). Accessed 26 June 2012
  14. 14.
    Demers, F., Malenfant, J.: Reflection in logic, functional and object-oriented programming: a short comparative study. In: Proceedings of the IJCAI, vol. 95, pp. 29–38 (1995)Google Scholar
  15. 15.
    Smith, B.C.: Reflection and semantics in LISP. In: Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’84, pp. 23–35. ACM, New York (1984)Google Scholar
  16. 16.
    Stump, A.: Directly reflective meta-programming. High. Order Symbolic Comput. 22(2), 115–144 (2009)CrossRefGoogle Scholar
  17. 17.
    Goldberg, A., Robson, D.: Smalltalk-80: The Language and Its Implementation. Addison-Wesley Longman Publishing Co. Inc., Boston (1983)zbMATHGoogle Scholar
  18. 18.
    Sheard, T.: Staged programming. http://web.cecs.pdx.edu/~sheard/staged.html. Accessed 20 Aug 2012
  19. 19.
    Altenkirch, T.: [Agda mailing list] More powerful quoting and reflection? mailing list communication. https://lists.chalmers.se/pipermail/agda/2012/004127.html (2012). Accessed 14 Sept 2012
  20. 20.
    Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reasoning 3(2), 95–152 (2010). (RR-7392 RR-7392)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  1. 1.Department of Computer ScienceUtrecht UniversityUtrechtThe Netherlands

Personalised recommendations