Frederik is a PhD student at the Technical University of Denmark. He comes from an electrical engineering background, and is interested in applying formal methods to safety critical distributed systems. To facilitate this, he works on making formal methods tools more applicable, easier to use, and easier to understand by building them on a foundation of functional programming. Before starting the PhD, he worked as a software developer in the travel industry and as a researcher at the Danish Cancer Society Research Center.
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. Our experience is that students grasp the meaning of programs quickly, and appreciate the precision available in the mechanized definitions and proofs.
Slides