Skip to Main content Skip to Navigation
Conference papers

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

David Pichardie 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : David Pichardie Connect in order to contact the contributor
Submitted on : Monday, October 20, 2008 - 4:47:57 PM
Last modification on : Friday, February 4, 2022 - 3:23:21 AM
Long-term archiving on: : Tuesday, October 9, 2012 - 2:01:29 PM


Files produced by the author(s)


  • HAL Id : inria-00332365, version 1


David Pichardie. Building certified static analysers by modular construction of well-founded lattices. Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), 2008, Shangai, China. ⟨inria-00332365⟩



Record views


Files downloads