SOAC's in Coq

I just recently completed by bachelors degree at DIKU, and my final project was about formalizing second-order array combinators using the Coq proof assistant.

Second-order array combinators

SOAC’s are limited versions of higher order functions on lists/arrays found in functional programmings languages like Haskell or ML.

In the case of map we limit disallow arbitrary function objects, and only allow syntactic lambda abstactions of the form

map (\x -> e) xs

To optimize programs written using these combinators, we have various fusion rules, for instance for map,

map g (map f xs) = map (g o f) xs

and for filter,

filter p (filter q xs) = filter (\x -> q && p) xs

The project

The work consisted of verifying these fusion rules by using various methods. The main idea was to formalize a simple programming language, and then verify that these transformations preserved the program semantics for all possible programs.

The formalization can be found here. All the details can be foun in the report here.