Sciweavers

ENTCS
2008

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

13 years 2 months ago
Building Certified Static Analysers by Modular Construction of Well-founded Lattices
This 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.
David Pichardie
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors David Pichardie
Comments (0)