A Deductive Verification Framework For Higher Order Programs

TL;DR

This paper proposes a framework based on defunctionalization and Why3 for the deductive verification of effectful higher-order programs, enabling the use of automated verifiers on transformed first-order code.

Contribution

It introduces a novel approach combining defunctionalization with Why3 to verify higher-order effectful programs automatically.

Findings

Defunctionalization effectively transforms higher-order programs into first-order form.

The framework leverages existing automated verifiers for correctness proofs.

Preliminary results show promise for automated verification of complex higher-order code.

Abstract

In this report, we present the preliminary work developed for our research project for the APDC (\'Area Pr\'atica de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for the verification of effectful higher-order programs. We use defunctionalization as an intermediate transformation from higher-order OCaml implementations into first order ones. The target for our translation is WhyML, the Why3's programming language. We believe defunctionalization can be an interesting route for the automated verification of higher-order programs, since one can employ off-the-shelf automated program verifiers to prove the correctness of the generated first-order program. This report also serves to introduce the reader to the subject of deductive program verification and some of the tools and concepts used to prove higher order effectful programs.