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 metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00332365
Contributor : David Pichardie <>
Submitted on : Monday, October 20, 2008 - 4:47:57 PM
Last modification on : Friday, November 16, 2018 - 1:24:24 AM
Long-term archiving on : Tuesday, October 9, 2012 - 2:01:29 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00332365, version 1

Citation

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⟩

Share

Metrics

Record views

427

Files downloads

188