A. Asperti, H. Geuvers, and R. Natarajan, Social processes, program veri cation and all that, Mathematical Structures in Computer Science, vol.19, issue.5, pp.877-896, 2009.

T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet et al., A formally veri ed compiler for Lustre, PLDI 2017: Proceedings of the 38th Conference on Programming Language Design and Implementation, pp.586-601, 2017.

A. Church, A note on the Entscheidungsproblem, J. Symb. Log, vol.1, issue.1, pp.40-41, 1936.

V. Cortier and S. Kremer, Formal models and techniques for analyzing security protocols: A tutorial, Foundations and Trends in Programming Languages, vol.1, issue.3, pp.151-267, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01090874

P. Cousot and R. Cousot, Abstract interpretation: A uni ed lattice model for static analysis of programs by construction or approximation of xpoints, POPL 1977: Conference Record of the Fourth Symposium on Principles of Programming Languages, pp.238-252, 1977.

H. B. Curry and R. Feys, Combinatory Logic, 1958.

M. Davis, The Universal Computer: The Road from Leibniz to Turing, 2012.

G. Dowek, Computation, Proof, Machine: Mathematics Enters a New Age, 2015.

E. A. Emerson and E. M. Clarke, Characterizing correctness properties of parallel programs using xpoints, Automata, Languages and Programming, vol.85, pp.169-181, 1980.

J. Filliâtre, Knuth's prime numbers, Gallery of verified programs

R. W. Floyd, Assigning meaning to programs, Mathematical Aspects of Computer Science, vol.19, pp.19-32, 1967.

H. H. Goldstine, The Computer from Pascal to von Neumann, 1980.

K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik, vol.38, pp.173-198, 1931.

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-585, 1969.

W. A. Howard, The formulae-as-types notion of construction, Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1969.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-veri ed C static analyzer, POPL 2015: Proceedings of the 42nd Symposium on Principles of Programming Languages, pp.247-259, 2015.

G. Katz, C. W. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, Reluplex: An e cient SMT solver for verifying deep neural networks, CAV 2017: Computer Aided Verification, 29th International Conference, vol.10426, pp.97-117, 2017.

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4: formal veri cation of an operating-system kernel, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.

D. E. Knuth, Fundamental Algorithms, vol.1, 1997.

G. Leibniz, Nova Methodus pro Maximis et Minimis. Acta Eruditorum, 1684.

X. Leroy, Formal veri cation of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.

X. Leroy, Le logiciel, entre l'esprit et la matière, Leçons inaugurales du Collège de France. Fayard, vol.284, 2019.

X. Leroy, Le logiciel, entre l'esprit et la matière, Leçons inaugurales du Collège de France. OpenEdition Books, vol.284, 2019.

I. L. Markov, Limits on fundamental limits to computation, Nature, vol.512, pp.147-154, 2014.

L. F. Menabrea and A. Augusta, Countess of Lovelace. Sketch of the analytical engine invented by Charles Babbage, p.1842

M. Moneghetti, Collège de France: 40 leçons inaugurales

L. Morris and C. B. Jones, An early program proof by Alan Turing, Ann. Hist. Computing, vol.6, issue.2, pp.129-143, 1984.

P. Mounier-kuhn, L'informatique en France de la seconde guerre mondiale au Plan Calcul: L'émergence d'une science, P. U. Paris-Sorbonne, 2010.

H. R. Nielson and F. Nielson, Semantics with Applications: An Appetizer, 2007.

C. , Weapons of Math Destruction: How Big Data Increases Inequality and Threatens Democracy. Crown, 2016.

D. A. Peled, Software Reliability Methods. Texts in Computer Science, 2001.

B. C. Pierce, Types and Programming Languages, 2002.

J. Queille and J. Sifakis, Speci cation and veri cation of concurrent systems in CESAR, International Symposium on Programming, 5th Colloquium, vol.137, pp.337-351, 1982.

L. Théry, Proving pearl: Knuth's algorithm for prime numbers, TPHOLs 2003: Theorem Proving in Higher Order Logics, vol.2758, pp.304-318, 2003.

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, issue.1, pp.230-265, 1937.

J. Van-de-meent, B. Paige, H. Yang, and F. Wood, An introduction to probabilistic programming, Computing Research Repository, 2018.

J. Van-heijenoort, From Frege to Gödel: A Source Book in Mathematical Logic, pp.1879-1931, 1977.