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

F. Besson, T. P. Jensen, D. Pichardie, and T. Turpin, Certified result checking for polyhedral analysis of bytecode programs, pp.253-267, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00537816

S. Boulmé, Intuitionistic Refinement Calculus, TLCA, LNCS, vol.4583, 2007.

S. Boulmé, What is the Foreign Function Interface of the Coq Programming Language? Talk at the Coq Workshop, 2018.

S. Boulmé and A. Maréchal, Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra, ITP, LNCS, vol.9236, 2015.

S. Boulmé and A. Maréchal, Toward Certification for Free! Preprint on, 2017.

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

P. Cousot, Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, TCS, vol.277, issue.1-2, 2002.

P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, 1977.

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, 1978.

E. W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, vol.18, issue.8, pp.453-457, 1975.

R. T. Farouki, The Bernstein polynomial basis: A centennial retrospective, Computer Aided Geometric Design, vol.29, issue.6, 2012.

A. Fouilhé and S. Boulmé, A certifying frontend for (sub)polyhedral abstract domains, VSTTE, LNCS, vol.8471, 2014.

A. Fouilhé, D. Monniaux, and M. Périn, Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra, In: SAS, vol.7935, 2013.

B. Grégoire and A. Mahboubi, Proving equalities in a commutative ring done right in Coq, TPHOL, LNCS, vol.3603, pp.98-113, 2005.

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

J. H. Jourdan, Verasco: a Formally Verified C Static Analyzer. Theses, 2016.
URL : https://hal.archives-ouvertes.fr/tel-01327023

J. H. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-verified C static analyzer, 2015.
DOI : 10.1145/2775051.2676966

URL : https://hal.archives-ouvertes.fr/hal-01078386

V. Laporte, Verified static analyzes for low-level languages, Theses, Université Rennes, vol.1, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01285624

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

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

URL : https://link.springer.com/content/pdf/10.1007%2F3-540-61055-3_39.pdf

A. Maréchal, New algorithmics for polyhedral calculus via parametric linear programm ing, 2017.

A. Maréchal, A. Fouilhé, T. King, D. Monniaux, and M. Périn, Polyhedral approximation of multivariate polynomials using Handelman's theorem, pp.166-184, 2016.

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

L. Mauborgne and X. Rival, Trace partitioning in abstract interpretation based static analyzers, ESOP'05, vol.3444, 2005.

A. Miné, Symbolic methods to enhance the precision of numerical abstract domains, VMCAI, LNCS, vol.3855, 2006.

C. Morgan, Prentice Hall International series in computer science, 1994.

M. M. Moscato, C. A. Muñoz, and A. P. Smith, Affine arithmetic and applications to real-number proving. In: ITP, LNCS, vol.9236, 2015.

J. C. Reynolds, The discoveries of continuations, Lisp and Symbolic Computation, vol.6, issue.3-4, 1993.

A. Spiwack, Abstract interpretation as anti-refinement, 2013.

, The Coq Development Team: The Coq proof assistant reference manual-version 8

P. Wadler, Monads for functional programming, AFP, LNCS, vol.925, 1995.