Lightweight Approaches to the Verification of Functional Programs

Abstract

The constraints of pure functional programs are often applauded for the resulting safety and correctness guarantees. It is also claimed that these programs are easier to reason about and, therefore, verify. Despite being taken as fact within the community, the availability of effective verification tools tells a different story. This thesis focuses on two verification problems specific to functional programs — pattern-match safety and functional correctness. We develop two automated, lightweight verification tools with a focus on performance.

The first problem is to verify that a given functional program does not crash due to inexhaustive pattern-matching expressions in a function’s definition. To this end, we present a refinement type system with a restricted form of structural subtyping and environment-level intersection. We describe a fully automated, sound and complete type inference procedure for this system which, under reasonable assumptions, is worst-case linear-time in the size of the program. Compositionality is essential to obtaining this complexity guarantee but is only enabled by the novel restriction we place on refinement types.

Other than expressive type systems, pure functional programs naturally lend themselves to equational specifications. These specifications are a desirable target for an automated verification tool because they are immediately accessible to the average programmer. Nevertheless, such a tool must tackle the thorny issue of proof by induction when verifying recursive programs over algebraic datatypes. We propose a new cyclic proof system that is well-adapted to equational reasoning over inductively defined datatypes. The key to our system is the way in which cyclic proofs and equational reasoning are mediated through the use of contextual substitution as a cut-like rule. We outline a performant proof search algorithm that relies on a number of supporting theoretical developments, including an alternative, incremental technique for checking the correctness of a candidate proof.

Date of Award	19 Mar 2024
Original language	English
Awarding Institution	University of Bristol
Supervisor	Steven Ramsay (Supervisor) & Luke Ong (Supervisor)