R. Abramsky, . Hankin, S. Abramsky, and C. Hankin, Abstract Interpretation of Declarative Languages, 1987.

J. Abramsky, S. Abramsky, A. Jung, S. Abramsky, D. Gabbay et al., Domain theory A General Framework for Semantics-Based Bottom-Up Abstract Interpretation of Logic Programs, Handbook of Logic in Computer Science ACM TOPLAS, vol.15, issue.1, pp.1-168133, 1993.

. Benton, Some Domain Theory and Denotational Semantics in Coq, pp.115-130, 2009.
DOI : 10.1007/3-540-60275-5_72

. Bertot, . Komendantsky, Y. Bertot, and V. Komendantsky, Fixed point semantics and partial recursion in Coq, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.89-96, 2008.
DOI : 10.1145/1389449.1389461
URL : https://hal.archives-ouvertes.fr/inria-00190975

. Besson, Certified Static Analysis by Abstract Interpretation, FOSAD, pp.223-257, 2009.
DOI : 10.1145/1146809.1146811
URL : https://hal.archives-ouvertes.fr/inria-00538753

. Besson, Proof-carrying code from certified abstract interpretation and fixpoint compression, Theoretical Computer Science, vol.364, issue.3, pp.273-291, 2006.
DOI : 10.1016/j.tcs.2006.08.012
URL : http://doi.org/10.1016/j.tcs.2006.08.012

M. Billaud, Simple operational and denotational semantics for Prolog with cut, Theoretical Computer Science, vol.71, issue.2, pp.193-208, 1990.
DOI : 10.1016/0304-3975(90)90197-P

G. Birkhoff, Lattice Theory, Colloquium Publications, 1967.
DOI : 10.1090/coll/025

. Blanqui, . Koprowski, F. Blanqui, and A. Koprowski, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04, pp.827-859, 2011.
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00543157

N. G. Bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem, INDAG. MATH, vol.34, pp.381-392, 1972.

. Cachera, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, pp.56-78, 2005.
DOI : 10.1016/j.tcs.2005.06.004
URL : https://hal.archives-ouvertes.fr/inria-00564633

P. Cachera, D. Cachera, and D. Pichardie, A Certified Denotational Abstract Interpreter, Proc. of the conference on Interactive Theorem Proving (ITP-10), pp.9-24, 2010.
DOI : 10.1007/978-3-642-14052-5_3
URL : https://hal.archives-ouvertes.fr/inria-00537810

J. Cheney, C. Urban, and A. Chlipala, ??Prolog: A Logic Programming Language with Names, Binding and ??-Equivalence, ICFP, pp.269-283, 2004.
DOI : 10.1007/978-3-540-27775-0_19

. Codish, Bottom-up abstract interpretation of logic programs, Theoretical Computer Science, vol.124, issue.1, pp.93-125, 1994.
DOI : 10.1016/0304-3975(94)90055-8

. Cousot, . Cousot, P. Cousot, R. Cousot, . De et al., Systematic Design of Program Analysis Frameworks Global Analysis of Constraint Logic Programs, POPL, pp.269-282564, 1979.

E. P. De-vink-de-vink, Comparative semantics for prolog with cut, Science of Computer Programming, vol.13, issue.2-3, pp.237-264, 1989.
DOI : 10.1016/0167-6423(90)90072-L

M. Debray, S. K. Debray, and P. Mishra, Denotational and operational semantics for prolog, The Journal of Logic Programming, vol.5, issue.1, pp.81-91, 1988.
DOI : 10.1016/0743-1066(88)90007-6

W. Drabent, Abstract, Theory and Practice of Logic Programming, vol.12, issue.06, pp.929-936, 2012.
DOI : 10.1016/0743-1066(91)90026-L

. Lambda-prolog, An Extended Logic Programming Language, Lecture Notes in Computer Science, vol.310, pp.754-755

. Gabbrielli, . Levi, M. Gabbrielli, G. Levi, and J. P. Gallagher, On the semantics of logic programs, ICALP, pp.1-19, 1991.
DOI : 10.1007/3-540-54233-7_121

R. Giacobazzi and G. Gonthier, Semantic Aspects of Logic Program Analysis The Four Colour Theorem: Engineering of a Formal Proof, Dipartimento di Informatica, p.333, 1993.

. Gonthier, A Machine-Checked Proof of the Odd Order Theorem, Proc. of the 4th conference on Interactive Theorem Proving, pp.163-17995, 2010.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

P. Hudak, A Semantic Model of Reference Counting and its Abstraction, Abstract Interpretation of Declarative Languages, pp.45-62, 1987.

B. Janssens, G. Janssens, and M. Bruynooghe, Deriving descriptions of possible values of program variables by means of abstract interpretation, The Journal of Logic Programming, vol.13, issue.2-3, pp.13205-258, 1992.
DOI : 10.1016/0743-1066(92)90032-X

. King, . Lu, A. King, and L. Lu, A backward analysis for constraint logic programs, Theory and Practice of Logic Programming, vol.2, issue.4-5, pp.4-5517, 2002.
DOI : 10.1017/S1471068402001436

. King, . Lu, A. King, and L. Lu, Forward versus Backward Verification of Logic Programs On notation for ordinal numbers, ICLP, pp.315-330, 1938.

. Klein, seL4, Communications of the ACM, vol.53, issue.6, pp.53107-115, 2010.
DOI : 10.1145/1743546.1743574

. Kriener, . King, J. Kriener, and A. King, Abstract, Proofs in CoRR volume abs, pp.537-553, 1109.
DOI : 10.1017/S1471068411000160

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

G. Levi, K. Muthukumar, and M. V. Hermenegildo, On the Semantics of Logic Programs Compile-Time Derivation of Variable Dependency Using Abstract Interpretation, ICLP, page 945, pp.13315-347, 1991.

E. Pfenning, F. Pfenning, and C. Elliott, Higher-Order Abstract Syntax, pp.199-208, 1988.

C. Pusch and R. Ramakrishnan, Verification of Compiler Correctness for the WAM Magic templates: A spellbinding approach to logic programs, TPHOLs, pp.347-361, 1991.

. Schrijvers, Abstract interpretation for constraint handling rules, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, pp.218-229, 2005.
DOI : 10.1145/1069774.1069795

. Berghofer, The Twelf Proof Assistant, pp.79-83, 2009.

D. Scott, Continuous lattices, 1971.
DOI : 10.1007/BFb0073967

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

. Van-emden, . Kowalski, M. H. Van-emden, and R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM, vol.23, issue.4, pp.733-742, 1976.
DOI : 10.1145/321978.321991