Teaching Functional Programmers Logic and Metatheory | Frederik Krogsdal Jacobsen | Making formal methods easier to understand ABSTRACT 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. Authors: Frederik Krogsdal Jacobsen and Jørgen Villadsen - Technical University of Denmark, Copenhagen, Denmark • Follow us on social: Twitter: https://twitter.com/LambdaDays LinkedIn: https://www.linkedin.com/company/lambda-days/ • Looking for a unique learning experience? Attend the next Code Sync conference near you! See what’s coming up at: https://codesync.global • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw