Mechanizing Hoare Style Proof Outlines for Imperative Programs in Agda
O.N. de Haas (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Arie van Van Deursen – Graduation committee member (TU Delft - Software Technology)
Robbert Krebbers – Graduation committee member (Radboud Universiteit Nijmegen)
Jesper Cockx – Graduation committee member (TU Delft - Programming Languages)
A.J. Rouvoet – Mentor
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof in the style of Hoare. This process has been mechanized by the introduction of Separation Logic and computer assisted verification tools. However, the tools fail to achieve the readability and convenience of manual paper proof outlines. This is a pity, because getting ideas and proofs across is essential for scientific research. I introduce a mechanization for proof outlines of imperative programs to interactively write human readable outlines in the dependently typed programming language and proof assistant Agda. I achieve this by introducing practical syntax and proof automation to write concise proof outlines for a simple imperative programming language based on λ-calculus. The proposed solution results in proof outlines that combine the readability of paper proof outlines and the precision of mechanization.