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.
Type de document :
Communication dans un congrès
Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS'08), 2008, Shangai, China. 2008
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00332365
Contributeur : David Pichardie <>
Soumis le : lundi 20 octobre 2008 - 16:47:57
Dernière modification le : mercredi 16 mai 2018 - 11:23:03
Document(s) archivé(s) le : mardi 9 octobre 2012 - 14:01:29

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00332365, version 1

Collections

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. 2008. 〈inria-00332365〉

Partager

Métriques

Consultations de la notice

403

Téléchargements de fichiers

117