This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Teaching Automated Reasoning and Formally Verified Functional Programming in Agda and Isabelle/HOL by Jørgen Villadsen ABSTRACT We formalize two micro provers for propositional logic in Isabelle/HOL and Agda. The provers are used in an automated reasoning course at DTU where they concretize discussions of soundness and completeness. The students are familiar with functional programming beforehand but formalizing the provers, and other programs, introduces the students to formally verified functional programming in a proof assistant. Proofs that have been informal in previous courses, for instance of termination, can now be verified by the machine, and the provers provide practical examples. Similarly, the formal meta-languages provided by the formalizations clarify boundaries that can be muddled with pen and paper, for instance between syntactic and semantic arguments. We find that the automation available in Isabelle/HOL provides succinctness while the verification in Agda closer resembles functional programming. --- SPEAKER - Jørgen Villadsen Formally Verified Functional Programming Jørgen Villadsen is Associate Professor at the Department of Applied Mathematics and Computer Science of the Technical University of Denmark (DTU). His research is in logic and artificial intelligence. He is currently teaching several programming courses and an automated reasoning course. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​