Social processes, program veri cation and all that, Mathematical Structures in Computer Science, vol.19, issue.5, pp.877-896, 2009. ,
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 note on the Entscheidungsproblem, J. Symb. Log, vol.1, issue.1, pp.40-41, 1936. ,
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
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. ,
Combinatory Logic, 1958. ,
The Universal Computer: The Road from Leibniz to Turing, 2012. ,
, Computation, Proof, Machine: Mathematics Enters a New Age, 2015.
Characterizing correctness properties of parallel programs using xpoints, Automata, Languages and Programming, vol.85, pp.169-181, 1980. ,
Knuth's prime numbers, Gallery of verified programs ,
Assigning meaning to programs, Mathematical Aspects of Computer Science, vol.19, pp.19-32, 1967. ,
The Computer from Pascal to von Neumann, 1980. ,
, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik, vol.38, pp.173-198, 1931.
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-585, 1969. ,
The formulae-as-types notion of construction, Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1969. ,
A formally-veri ed C static analyzer, POPL 2015: Proceedings of the 42nd Symposium on Principles of Programming Languages, pp.247-259, 2015. ,
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. ,
seL4: formal veri cation of an operating-system kernel, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010. ,
, Fundamental Algorithms, vol.1, 1997.
Nova Methodus pro Maximis et Minimis. Acta Eruditorum, 1684. ,
Formal veri cation of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
Le logiciel, entre l'esprit et la matière, Leçons inaugurales du Collège de France. Fayard, vol.284, 2019. ,
Limits on fundamental limits to computation, Nature, vol.512, pp.147-154, 2014. ,
Countess of Lovelace. Sketch of the analytical engine invented by Charles Babbage, p.1842 ,
Collège de France: 40 leçons inaugurales ,
An early program proof by Alan Turing, Ann. Hist. Computing, vol.6, issue.2, pp.129-143, 1984. ,
L'informatique en France de la seconde guerre mondiale au Plan Calcul: L'émergence d'une science, P. U. Paris-Sorbonne, 2010. ,
, Semantics with Applications: An Appetizer, 2007.
Weapons of Math Destruction: How Big Data Increases Inequality and Threatens Democracy. Crown, 2016. ,
Software Reliability Methods. Texts in Computer Science, 2001. ,
Types and Programming Languages, 2002. ,
Speci cation and veri cation of concurrent systems in CESAR, International Symposium on Programming, 5th Colloquium, vol.137, pp.337-351, 1982. ,
Proving pearl: Knuth's algorithm for prime numbers, TPHOLs 2003: Theorem Proving in Higher Order Logics, vol.2758, pp.304-318, 2003. ,
On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, issue.1, pp.230-265, 1937. ,
An introduction to probabilistic programming, Computing Research Repository, 2018. ,
From Frege to Gödel: A Source Book in Mathematical Logic, pp.1879-1931, 1977. ,