Inducing students to induct
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.
KeywordsTheorem Prover Duality Theorem Functional Programming Functional Language Arithmetic Expression
Unable to display preview. Download preview PDF.
- 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.Robert Boyer and J. S. Moore. A Computational Logic Handbook. Academic Press, 1988.Google Scholar
- 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.A.J. Field and P.G. Harrison. Functional Programming. Addison-Wesley International Computer Science Series, 1988.Google Scholar
- 5.H. Glaser, C. Hankin, and D. Till. Principles of Functional Programming. Prentice-Hall International, Inc., London, 1984.Google Scholar
- 6.D Harel. Algorithmics: the Spirit of Computing. Addison-Wesley, 1987.Google Scholar
- 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.D.R. Lester. CS412 — Algorithmics and Functions. Course notes, University of Manchester, 1992.Google Scholar
- 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.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.H.R. Nielson and F. Nielson. Semantics with applications: a formal introduction. Wiley, 1992.Google Scholar
- 12.L.C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994.Google Scholar
- 13.R. Plasmeijer and M. van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison-Wesley, 1993.Google Scholar
- 14.C. Reade. Elements of Functional Programming. International Computer Science Series. Addison-Wesley, 1989.Google Scholar
- 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