Tutorial implementation of Hoare logic in Haskell

TL;DR

This paper presents a Haskell-based implementation of propositional calculus, number theory, and a simple imperative language, culminating in a Hoare logic system for reasoning about program correctness without full execution.

Contribution

It introduces a novel Haskell implementation of Hoare logic enabling formal reasoning about programs in a practical setting.

Findings

Implementation of propositional calculus, number theory, and imperative language in Haskell

Development of a Hoare logic system for program verification

Enables deduction of program facts without full evaluation

Abstract

Using the programming language Haskell, we introduce an implementation of propositional calculus, number theory, and a simple imperative language that can evaluate arithmetic and boolean expressions. Finally, we provide an implementation of Hoare's logic which will allow us to deduce facts about programs without the need for a full evaluation.