Teaching Functional Programmers Logic and Metatheory

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

52 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings of Tenth and Eleventh International Workshop on Trends in Functional Programming In Education
EditorsP. Achten, E. Machkasova
Publication date2022
Publication statusPublished - 2022
EventTrends in Functional Programming in Education 2022 - Virtual event
Duration: 16 Mar 202216 Mar 2022


ConferenceTrends in Functional Programming in Education 2022
LocationVirtual event
SeriesElectronic Proceedings in Theoretical Computer Science


Dive into the research topics of 'Teaching Functional Programmers Logic and Metatheory'. Together they form a unique fingerprint.

Cite this