R. J. Back and J. Von-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.
DOI : 10.1007/978-3-540-31987-0_23
URL : https://hal.archives-ouvertes.fr/inria-00537816

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

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

S. Boulmé and A. Maréchal, Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra, ITP, 2015.
DOI : 10.1007/978-3-319-22102-1_7

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

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

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-00930103

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

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

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

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

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

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

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, 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

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

S. Liang and P. Hudak, Modular denotational semantics for compiler construction, pp.219-234, 1996.
DOI : 10.1007/3-540-61055-3_39
URL : http://java.sun.com/people/sl/papers/esop96.ps.gz

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.
DOI : 10.1007/978-3-662-49122-5_8

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

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

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

M. M. Moscato, C. A. Muñoz, and A. P. Smith, Affine Arithmetic and Applications to Real-Number Proving, ITP, LNCS, 2015.
DOI : 10.1007/978-3-319-22102-1_20

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

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

P. Wadler, Monads for functional programming, AFP, LNCS, 1995.
DOI : 10.1007/3-540-59451-5_2
URL : http://flint.cs.yale.edu/trifonov/cs629/WadlerMonadsForFP.pdf