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.

Teaching Automated Reasoning and Formally Verified Functional Programming in Agda and Isabelle/HOL

AUTHORS: Asta Halkjær From, Jørgen Villadsen  

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.

Slides
←Back