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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 10th International Workshop on Trends in Functional Programming in Education |
| Number of pages | 20 |
| Publication date | 2021 |
| Publication status | Published - 2021 |
| Event | 10th International Workshop on Trends in Functional Programming in Education - Virtual Event Duration: 16 Feb 2021 → 16 Feb 2021 |
Conference
| Conference | 10th International Workshop on Trends in Functional Programming in Education |
|---|---|
| Location | Virtual Event |
| Period | 16/02/2021 → 16/02/2021 |