S. Abramsky, Domain Theory in Logical Form, Annals of Pure and Applied Logic, vol.51, pp.1-2, 1991.

F. Oana, T. Andreescu, S. Jensen, B. Lescuyer, and . Montagu, Inferring Frame Conditions with Static Correlation Analysis, Proc. ACM Program. Lang. 3, POPL, Article, vol.47, 2019.

B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich, Engineering Formal Metatheory, Proceedings of the 35 th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages -POPL '08, 2008.

A. Banerjee and T. Jensen, Modular Control-Flow Analysis with Rank 2 Intersection Types, Mathematical Structures in Computer Science, vol.13, pp.87-124, 2003.

M. Barnett, -. Bor, R. Chang, B. Deline, K. Jacobs et al., Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Formal Methods for Components and Objects, vol.4111, 2006.

M. Barnett, K. Rustan, M. Leino, and W. Schulte, The Spec# Programming System: An Overview, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, vol.3362, 2005.

R. Bird and . Oege-de-moor, The Algebra of Programming, 1996.

D. Cachera and D. Pichardie, A Certified Denotational Abstract Interpreter, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00537810

A. Charguéraud, Program Verification through Characteristic Formulae, Proceedings of the 15 th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), 2010.

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.49, issue.3, 2011.

A. Stephen and . Cook, Soundness and Completeness of an Axiom System for Program Verification, SIAM J. Comput, vol.7, pp.70-90, 1978.

P. Cousot, Types as Abstract Interpretations, Proceedings of the 24 th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages -POPL '97, 1997.

P. Cousot and R. Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints, Proceedings of the 4 th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '77), 1977.

P. Cousot and R. Cousot, Higher-Order Abstract Interpretation (and Application to Comportment Analysis Generalizing Strictness, Termination, Projection and PER Analysis of Functional Languages), Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL94), 1994.

P. Cousot and R. Cousot, Modular Static Program Analysis, Compiler Construction, vol.2304, pp.159-179, 2002.

M. Das, Unification-Based Pointer Analysis with Directional Assignments, Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI '00), 2000.

D. Dreyer, K. Crary, and R. Harper, A Type System for Higher-Order Modules, Proceedings of the 30 th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '03), 2003.

C. Earl, M. Might, and D. Van-horn, Pushdown Control-Flow Analysis of Higher-Order Programs, 2010.

A. Farzan and Z. Kincaid, Compositional Recurrence Analysis, Proceedings of the 15 th Conference on Formal Methods in Computer-Aided Design (FMCAD '15), 2015.

J. , C. Filliâtre, and A. Paskevich, Why3 Ð Where Programs Meet Provers, Programming Languages and Systems, vol.7792, 2013.

R. W. Floyd, Assigning Meanings to Programs, Program Verification, 1993.

M. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax Involving Binders, Proceedings. 14 th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.

L. Gu, A. Vaynberg, B. Ford, Z. Shao, and D. Costanzo, CertiKOS: A Certified Kernel for Secure Cloud Computing, Proceedings of the Second Asia-Pacific Workshop on Systems -APSys '11, 2011.

N. Heintze, Set-Based Analysis of ML Programs, ACM SIGPLAN Lisp Pointers VII, vol.3, 1994.

C. A. Hoare, An Axiomatic Basis for Computer Programming, Commun. ACM, vol.12, pp.576-580, 1969.

K. Honda, M. Berger, and N. Yoshida, Descriptive and Relative Completeness of Logics for Higher-Order Functions, Automata, Languages and Programming, 2006.

D. Van-horn and M. Might, Abstracting Abstract Machines, Proceedings of the 15 th ACM SIGPLAN international conference on Functional programming -ICFP '10, 2010.

P. Hudak and J. Young, Collecting Interpretations of Expressions, ACM Transactions on Programming Languages and Systems, vol.13, issue.2, 1991.

H. Illous, M. Lemerre, and X. Rival, A Relational Shape Abstract Domain, NASA Formal Methods (LNCS, vol.10227, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01648681

B. Jeannet, A. Loginov, T. Reps, and M. Sagiv, A Relational Approach to Interprocedural Shape Analysis, Static Analysis, vol.3148, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00786335

D. Neil, S. S. Jones, and . Muchnick, Complexity of Flow Analysis, Inductive Assertion Synthesis and a Language Due to Dijkstra, 21 st Annual Symposium on Foundations of Computer Science (sfcs, 1980.

D. Neil, A. Jones, and . Mycroft, Data Flow Analysis of Applicative Programs Using Minimal Function Graphs, Proceedings of the 13 th ACM SIGACT-SIGPLAN symposium on Principles of programming languages -POPL '86, 1986.

G. Kahn, Natural Semantics, STACS 87, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075953

G. Kaki and S. Jagannathan, A Relational Framework for Higher-Order Shape Analysis, Proceedings of the 19 th ACM SIGPLAN International Conference on Functional Programming, 2014.

Z. Kincaid, J. Breck, A. F. Boroujeni, and T. Reps, Compositional Recurrence Analysis Revisited, Proceedings of the 38 th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017.

G. Klein, M. Norrish, T. Sewell, H. Tuch, S. Winwood et al., 2009. seL4: Formal Verification of an OS Kernel, Proceedings of the ACM SIGOPS 22 nd symposium on Operating systems principles -SOSP '09
URL : https://hal.archives-ouvertes.fr/hal-01582299

A. Saul and . Kripke, Semantical Analysis of Intuitionistic Logic I, Formal Systems and Recursive Functions, pp.71685-71694, 1965.

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: A Verified Implementation of ML, Proceedings of the 41 st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14), 2014.

X. Leroy, A Modular Module System, Journal of Functional Programming, vol.10, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00073825

X. Leroy, Formal Certification of a Compiler Back-End or: Programming a Compiler with a Proof Assistant, Conference record of the 33 rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages -POPL'06, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00000963

C. Marché and C. Paulin-mohring, Reasoning About Java Programs with Aliasing and Frame Conditions, Theorem Proving in Higher Order Logics, vol.3603, 2005.

B. Meyer, Framing the Frame Problem, Dependable Software Systems Engineering. 193?203, 2015.

, Control-Flow Analysis of Functional Programs, Comput. Surveys, vol.44, pp.1-33, 2012.

J. Midtgaard and T. Jensen, A Calculational Approach to Control-Flow Analysis by Abstract Interpretation, Static Analysis, 2008.

J. Midtgaard and T. P. Jensen, Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation, Proceedings of the 14 th ACM SIGPLAN international conference on Functional programming -ICFP '09, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00328154

F. Nielson, Hanne Riis Nielson, and Chris Hankin, 1999.

A. Pitts, Nominal Techniques. ACM SIGLOG News, vol.3, issue.1, 2016.

J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings 17 th Annual IEEE Symposium on Logic in Computer Science, 2002.

P. M. Rondon, M. Kawaguci, and R. Jhala, Liquid Types, Proceedings of the 29 th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '08), 2008.

O. Shivers, The Semantics of Scheme Control-Flow Analysis, Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '91), 1991.

A. Christopher, R. Stone, and . Harper, Extensional Equivalence and Singleton Types, ACM Transactions on Computational Logic, vol.7, issue.4, pp.676-722, 2006.

C. Urban and C. Kaliszyk, General Bindings and Alpha-Equivalence in Nominal Isabelle, Logical Methods in Computer Science, vol.8, issue.2, 2012.

J. Van-benthem, The Information in Intuitionistic Logic, Synthese, vol.167, pp.251-270, 2008.

N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. , Refinement Types for Haskell, Proceedings of the 19 th ACM SIGPLAN International Conference on Functional Programming -ICFP '14, 2014.

N. Vazou, A. Tondwalkar, V. Choudhury, R. G. Scott, R. R. Newton et al., Refinement Reflection: Complete Verification with SMT, Proceedings of the ACM on Programming Languages 2, POPL, p.31, 2017.