Building Certified Static Analysers by Modular Construction of Well-founded Lattices

AbstractThis 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 demonstrates the ability of the recent Coq module system in manipulating algebraic structures and extracting efficient Ocaml implementations from them. The second contribution of this work is a generic result, based on the constructive notion of accessibility predicate, about preservation of accessibility properties when combining relations