%0 Journal Article 
%F cachera05a
%A Cachera, D.
%A Jensen, T.
%A Pichardie, D.
%A Rusu, V.
%T Extracting a data flow analyser in constructive logic
%J Theoretical Computer Science
%V 	 342
%N 1
%P 56-78
%X A constraint-based data flow analysis is formalised in the specification language of the Coq proof assistant. This involves defining a dependent type of lattices together with a library of lattice functors for modular construction of complex abstract domains. Constraints are represented in a way that allows for both efficient constraint resolution and correctness proof of the analysis with respect to an operational semantics. The proof of existence of a solution to the constraints is constructive which means that the extraction mechanism of Coq provides a provably correct data flow analyser in Ocaml from the proof. The library of lattices and the representation of constraints are defined in an analysis-independent fashion that provides a basis for a generic framework for proving and extracting static analysers in Coq
%U 		 http://www.irisa.fr/vertecs/Publis/Ps/2005-TCS.pdf
%U http://dx.doi.org/10.1016/j.tcs.2005.06.004
%8 September
%D 2005