Inducing students to induct

  • David Lester
  • Sava Mintchev
Understanding LOLITA
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1022)


One of the problems encountered with a formal approach to the teaching of functional programming is to encourage students to perform inductive proofs for recursively defined functions. In this paper we investigate the use of a theorem prover (written in Haskell) to help students gain confidence in their mathematical abilities.

As examples, we use the material that we have developed for an introductory functional programming module; and show how the theorem prover can be of assistance.


Theorem Prover Duality Theorem Functional Programming Functional Language Arithmetic Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R.J. Bird and P.L. Wadler. An Introduction to Functional Programming. Prentice-Hall Series in Computer Science. Prentice-Hall International (UK) Ltd., Hemel Hempstead, Hertfordshire, England, 1988.Google Scholar
  2. 2.
    Robert Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, 1988.Google Scholar
  3. 3.
    P.J. Brumfitt. Metamorph — a formal methods toolkit with application to the design of digital hardware. Journal of Functional Programming, 2(4):437–473, October 1992.Google Scholar
  4. 4.
    A.J. Field and P.G. Harrison. Functional Programming. Addison-Wesley International Computer Science Series, 1988.Google Scholar
  5. 5.
    H. Glaser, C. Hankin, and D. Till. Principles of Functional Programming. Prentice-Hall International, Inc., London, 1984.Google Scholar
  6. 6.
    D Harel. Algorithmics: the Spirit of Computing. Addison-Wesley, 1987.Google Scholar
  7. 7.
    D.R. Lester. Combinator Graph Reduction: A Congruence and its Applications. Dphil thesis, Oxford University, 1988. Also published as Technical Monograph PRG-73.Google Scholar
  8. 8.
    D.R. Lester. CS412 — Algorithmics and Functions. Course notes, University of Manchester, 1992.Google Scholar
  9. 9.
    D.R. Lester and S. Mintchev. Towards machine-checked compiler correctness for higher-order pure functional languages. In L. Pacholski and J. Tiuryn, editors, Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic, pages 369–381. Springer-Verlag LNCS 933, 1995.Google Scholar
  10. 10.
    S. Mintchev. Mechanized reasoning about functional programs. In K. Hammond, D.N. Turner, and P. Sansom, editors, Functional Programming, Glasgow 1994, pages 151–167. Springer-Verlag Workshops in Computing, 1994.Google Scholar
  11. 11.
    H.R. Nielson and F. Nielson. Semantics with applications: a formal introduction. Wiley, 1992.Google Scholar
  12. 12.
    L.C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994.Google Scholar
  13. 13.
    R. Plasmeijer and M. van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, 1993.Google Scholar
  14. 14.
    C. Reade. Elements of Functional Programming. International Computer Science Series. Addison-Wesley, 1989.Google Scholar
  15. 15.
    C. Runciman, I. Toyn, and M. Firth. An incremental, exploratory and transformational environment for lazy functional programming. Journal of Functional Programming, 3(1):93–117, January 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • David Lester
    • 1
  • Sava Mintchev
    • 1
  1. 1.Department of Computer ScienceManchester UniversityManchesterUK

Personalised recommendations