Building certified static analysers by modular construction of well-founded lattices

International audienceThis paper presents fixpoint calculations on lattice structures as example of highly modular programming in a dependently typed functional language. We propose a library of Coq module functors for constructing complex lattices using efficient data structures. The lattice signature contains a well-foundedness proof obligation which ensures termination of generic fixpoint iteration algorithms. With this library, complex well-foundedness proofs can hence be constructed in a functorial fashion. This paper contains two distinct contributions. We first demonstrate the ability of the recent Coq module system in manipulating alge- braic structures and extracting efficient Ocaml implementations from them. The second contribution is a generic result, based on the constructive notion of accessibility predicate, about preservation of accessibility properties when combining relations