S. Boulmé and M. Alexandre, Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra, In: ITP. LNCS, vol.9236, 2015.
DOI : 10.1007/978-3-319-22102-1_7

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78, 1978.
DOI : 10.1145/512760.512770

A. Miné, Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, LNCS, vol.3855, 2006.
DOI : 10.1007/11609773_23

A. Fouilhé, D. Monniaux, and M. Périn, Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra, In: SAS, vol.7935, 2013.
DOI : 10.1007/978-3-642-38856-9_19

A. Fouilhé and S. Boulmé, A Certifying Frontend for (Sub)polyhedral Abstract Domains, LNCS, vol.8471, 2014.
DOI : 10.1007/978-3-319-12154-3_13

J. H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01078386

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

F. Besson, T. P. Jensen, D. Pichardie, and T. Turpin, Certified Result Checking for Polyhedral Analysis of Bytecode Programs, In: TGC, pp.253-267, 2010.
DOI : 10.1007/978-3-642-15640-3_17
URL : https://hal.archives-ouvertes.fr/inria-00537816

A. Maréchal and M. Périn, Three linearization techniques for multivariate polynomials in static analysis using convex polyhedra, Verimag Research Report, 2014.

R. J. Back and J. Von-wright, Refinement calculus -a systematic introduction. Graduate texts in computer science, 1999.

J. C. Reynolds, The discoveries of continuations, LISP and Symbolic Computation, vol.24, issue.3, pp.3-4, 1993.
DOI : 10.1007/BF01019459

P. Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, vol.277, issue.1-2, 2002.
DOI : 10.1016/S0304-3975(00)00313-3

A. Spiwack, Abstract interpretation as anti-refinement, p.4283, 1310.

E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, vol.18, issue.8, pp.453-457, 1975.
DOI : 10.1145/360933.360975

P. Wadler, Monads for functional programming, In: AFP. LNCS, vol.925, 1995.
DOI : 10.1007/3-540-59451-5_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.9674

S. Boulmé and A. Maréchal, A refinement calculus to certify impure abstract computations of the Verimag Polyhedra Library ? documentation and Coq+OCaml sources, 2015.

L. Mauborgne and X. Rival, Trace Partitioning in Abstract Interpretation Based Static Analyzers, ESOP'05, 2005.
DOI : 10.1007/978-3-540-31987-0_2

R. T. Farouki, The Bernstein polynomial basis: A centennial retrospective, Computer Aided Geometric Design, vol.29, issue.6, 2012.
DOI : 10.1016/j.cagd.2012.03.001

D. Handelman, Representing polynomials by positive linear functions on compact convex polyhedra, Pacific Journal of Mathematics, vol.132, issue.1, 1988.
DOI : 10.2140/pjm.1988.132.35

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, In: TPHOL, pp.98-113, 2005.
DOI : 10.1007/11541868_7

S. Liang and P. Hudak, Modular denotational semantics for compiler construction, pp.219-234, 1996.
DOI : 10.1007/3-540-61055-3_39

T. Braibant and D. Pous, Deciding Kleene Algebras in Coq, Logical Methods in Computer Science, vol.8, issue.1, 2012.
DOI : 10.2168/LMCS-8(1:16)2012
URL : https://hal.archives-ouvertes.fr/hal-00383070

S. Boulmé, Intuitionistic Refinement Calculus, In: TLCA, 2007.
DOI : 10.1007/978-3-540-73228-0_6