Proving Regular Theorems on Functional Programs

For several years, we develop a framework for automatically proving properties on higher-order functional programs [1,2] using tree automata, i.e., automata that recognize Regular Tree Languages. Basically, for a given functional program (possibly with higher-order functions) and a regular infinite set of inputs, our algorithm is abble to give a precise regular approximation of the set of outputs. Then, using standard algorithms on tree automata, it is possible to formally prove that the program is correct by checking that the output approximation does not contain errors or unexpected values. Unlike other existing automatic verification techniques (like F* or LiquidHaskell) which target numerical properties, using regular tree language makes it possible to prove structural properties on the outputs, i.e., prove properties on the algebraic datatypes manipulated by the program.

Thanks to abstract interpretation it is possible to extend the scope of properties that we can prove using regular approximations. Thus, we can provide a regular infinite set of *abstract inputs* and obtain a regular approximation of *abstract outputs*. For instance, to prove that a function sorts polymorphic lists of type List[T] (the concrete input) it can be sufficient to prove a property on a list of booleans List[Bool] (one possible abstraction). This is known as Knuth's 0-1-principle [3] (for a short presentation see [4], section 4). However, depending on the function and on the property to prove, lifting the property from the abstract world (e.g. List[Bool]) to the concrete world (e.g. List[T]) can be incorrect.

The objective of this PhD thesis is twofold. The first one is practical. It aims at investigating how to make such regular approximations scalable on real-size code programmed in real-life functional programming languages. The second is to find an algorithm to automatically check if lifting the proof carried out at the abstract level to the concrete level is correct. A good starting point is the study of similar successful attempts: theorems for sorting functions (in Knuth's 0-1 principle), Wadlers' Theorems for Free inferring generic theorems from types of functions [5] or Bernardy-Jansson-Claessen building theorems from a finite set of tests [6]. The PhD candidate
will search for generalizations of those principles. In the end, for a given function, property and abstraction, we want an algorithm checking if the proof of the property performed at the abstract level (using regular approximations and abstractions) is valid at the concrete level.