Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematics of Program Construction

MPC 2015: Mathematics of Program Construction pp 276–301Cite as

Auto in Agda

Programming Proof Search Using Reflection

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9129))

Abstract

As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    See https://github.com/wenkokke/AutoInAgda.

  2. 2.

    Note that Agda’s reflection mechanism should not be confused with ‘proof by reflection’ – the technique of writing a verified decisionprocedure for some class of problems.

  3. 3.

    Syntax for Agda tactics was added in Agda 2.4.2.

References

  • Agda development team. Agda release notes documenting the reflection mechanism. The Agda Wiki (2013). 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. Accessed 9 Feb 2013

  • Allais, G.: Proof automatization using reflection (implementations in Agda). MSc Intern report, University of Nottingham (2010)

    Google Scholar 

  • Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 9, 23:552–593 (2013). doi:10.1017/S095679681300018X

    Article  MathSciNet  MATH  Google Scholar 

  • Braibant, T.: Emancipate yourself from LTac (2012). http://gallium.inria.fr/blog/your-first-coq-plugin/

  • Chapman, J.: Type checking and normalisation. Ph.D. thesis, University of Nottingham (2009)

    Google Scholar 

  • Chlipala, A.: Certified Programming with Dependent Types. MIT Press, Cambridge (2013)

    Book  MATH  Google Scholar 

  • Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93–109. Springer, Heidelberg (2007). doi:10.1145/2500365.2500575

    Chapter  Google Scholar 

  • Coq development team. The Coq proof assistant reference manual. Logical Project (2004)

    Google Scholar 

  • Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP 2013). ACM, September 2013. doi:10.1145/2500365.2500575

  • Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York (1993)

    MATH  Google Scholar 

  • Lindblad, F., Benke, M.: A tool for automated theorem proving in Agda. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 154–169. Springer, Heidelberg (2006)

    Chapter  MATH  Google Scholar 

  • Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 374–389. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  • 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. (1985)

    Google Scholar 

  • McBride, C.: First-order unification by structural recursion. J. Funct. Program. 11, 13:1061–1075 (2003). doi:10.1017/S0956796803004957

    Article  MathSciNet  MATH  Google Scholar 

  • McBride, C.: Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation. In: Proceedings of the 6th ACM SIGPLAN Workshop on Generic Programming, WGP 2010, pp. 1–12. ACM, New York (2010). doi:10.1145/1863495.1863497

  • 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 (2007)

    Google Scholar 

  • Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009a)

    Chapter  MATH  Google Scholar 

  • Norell, U.: Playing with Agda. Invited talk at TPHOLS (2009b)

    Google Scholar 

  • Oury, N., Swierstra, W.: The power of Pi. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pp. 39–50 (2008). doi:10.1145/1411204.1411213

  • Jones, S.P. (ed.): Haskell 98 Language and Libraries: the Revised report. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  • Pitman, K.M.: Special forms in LISP. In: Proceedings of the 1980 ACM Conference on LISP and Functional Programming, pp. 179–187. ACM (1980)

    Google Scholar 

  • Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pp 1–16 (2002). doi:10.1145/581690.581691

  • Stutterheim, J., Swierstra, W., Swierstra, D.: Forty hours of declarative programming: teaching prolog at the junior college Utrecht. In: Proceedings First International Workshop on Trends in Functional Programming in Education, Electronic Proceedings in Theoretical Computer Science, University of St. Andrews, Scotland, UK, 11 June 2012, vol. 106, pp 50–62 (2013)

    Google Scholar 

  • Swierstra, W.: More dependent types for distributed arrays. High.-Ord. Symbol. Comput. 23(4), 489–506 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  • Swierstra, W., van Noort, T.: A library for polymorphic dynamic typing. J. Funct. Program. 23, 229–248 (2013). doi:10.1017/S0956796813000063

    Article  MATH  Google Scholar 

  • 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 1997 (1997). doi:10.1145/258993.259019

  • van der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  • van der Walt, P.: Reflection in Agda. Master’s thesis, Department of Computer Science, Utrecht University, Utrecht, The Netherlands (2012). http://igitur-archive.library.uu.nl/student-theses/2012-1030-200720/UUindex.html

  • Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp 87–100 (2013). doi:10.1145/2500365.2500579

Download references

Acknowledgements

We would like to thank the Software Technology Reading Club at the Universiteit Utrecht, and all our anonymous reviewers for their helpful feedback – we hope we have done their feedback justice.

Author information

Authors and Affiliations

  1. Universiteit Utrecht, Utrecht, The Netherlands

    Wen Kokke & Wouter Swierstra

Authors
  1. Wen Kokke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wouter Swierstra
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wen Kokke .

Editor information

Editors and Affiliations

  1. University of Oxford, Oxford, UK

    Ralf Hinze

  2. University of Bonn, Bonn, Germany

    Janis Voigtländer

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Kokke, W., Swierstra, W. (2015). Auto in Agda. In: Hinze, R., Voigtländer, J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science(), vol 9129. Springer, Cham. https://doi.org/10.1007/978-3-319-19797-5_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19797-5_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19796-8

  • Online ISBN: 978-3-319-19797-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation