Teaching Functional Programmers Logic and Metatheory

Frederik Krogsdal Jacobsen
(Technical University of Denmark)
Jørgen Villadsen
(Technical University of Denmark)

We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof assistant Isabelle/HOL. This allows us to make notions which are often unclear in textbooks precise, to experiment with definitions by executing them, and to prove metatheoretical theorems in full detail. We have surveyed student perceptions of our teaching approach to determine its usefulness and found that students felt that our formalizations helped them understand concepts in logic, and that they experimented with them as a learning tool. However, the approach was not enough to make students feel confident in their abilities to design and implement their own formal systems. Further studies are needed to confirm and generalize the results of our survey, but our initial results seem promising.

In Peter Achten and Elena Machkasova: Proceedings Tenth and Eleventh International Workshop on Trends in Functional Programming In Education (TFPIE 2021/22), Kraków, Poland (online), 16th February 2021/16th March 2022, Electronic Proceedings in Theoretical Computer Science 363, pp. 74–92.
Published: 26th July 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.363.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org