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

Asta Halkjær From, Jørgen Villadsen*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

15 Downloads (Pure)

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 languageEnglish
Title of host publicationProceedings of the 10th International Workshop on Trends in Functional Programming in Education
Number of pages20
Publication date2021
Publication statusPublished - 2021
Event10th International Workshop on Trends in Functional Programming in Education - Virtual Event
Duration: 16 Feb 202116 Feb 2021

Conference

Conference10th International Workshop on Trends in Functional Programming in Education
LocationVirtual Event
Period16/02/202116/02/2021

Fingerprint

Dive into the research topics of 'Teaching Automated Reasoning and Formally Verified Functional Programming in Agda and Isabelle/HOL'. Together they form a unique fingerprint.

Cite this