Conference paper
Tautology Checkers in Isabelle and Haskell
With the purpose of teaching functional programming and automated reasoning to computer science students, we formally verify a sound, complete and terminating tautology checker in Isabelle with code generation to Haskell. We describe a series of approaches and finish with a formalization based on formulas in negation normal form where the Isabelle/HOL functions consist of just 4 lines and the Isabelle/HOL proofs also consist of just 4 lines.
We investigate the generated Haskell code and present a 24-line manually assembled program.
Language: | English |
---|---|
Publisher: | CEUR-WS |
Year: | 2020 |
Pages: | 327-341 |
Proceedings: | 35<sup>th</sup> Edition of the Italian Conference on Computational Logic |
Series: | Ceur Workshop Proceedings |
ISSN: | 16130073 |
Types: | Conference paper |
ORCIDs: | Villadsen, Jørgen |