Rencontre, 4 avril 2019
Programme
- 10:30 – 12:00
-
Xavier Leroy (Collège de France, INRIA)
(Joint work with Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, and David Pichardie)
Static analysis is the automatic inference and checking of simple properties of all executions of a program. Initially developed in the context of compilers to support code optimization, static analysis is successful today for the formal verification of safety properties of critical software.
Abstract interpretation provides an elegant, powerful mathematical framework to define and reason about static analyses. However, the classic presentation for abstract interpretation, based on Galois connections, is set-theoretic and not constructive. This is an issue when one wants to verify a static analyzer using Coq, Agda, or other provers based on type theory.
In this talk, I will present a type-theoretic account of abstract interpretation, originally developed by David Pichardie, and show how it scales up to the verification of Verasco, a realistic static analyzer for the C language that has been developed and proved correct using Coq as a programming language and as a proof assistant.
For more information: http://compcert.inria.fr/verasco/
- 14:00 – 15:00
-
Raphaëlle Crubillé (IRIF, Univ. Paris Diderot)
The category of probabilistic coherence spaces (PCoh_!), introduced by Danos and Ehrhard, is a fully abstract model for PCF with discrete probabilities, where morphisms can be seen as power series. The category Cstab_m, of measurable cones and measurable stable functions, has been introduced by Ehrhard, Pagani and Tasson as a model for PCF with continuous probabilities.
In this talk, we will study the shape of stable functions when they are between discrete cones: we will show that they can actually be seen as generalized power series. The proof is based on a generalization of a theorem from real analysis due to Bernstein, that states that all absolutely monotonous functions on reals are power series. From there, we will build a full and faithful functor from PCoh_! into Cstab_m that moreover preserves the cartesian closed structure.
- 15:30 – 16:30
-
Ludovic Patey (CNRS, Institut Camille Jordan)Invited talk: Introduction to reverse mathematics
Reverse mathematics is a fundational program whose goal is to find op- timal axioms to prove ordinary theorems. They use the framework of second- order arithmetics, with a base theory, RCA 0 , capturing computable mathematics. Started in the 70s by Harvey Friedman, they revealed five big systems of axioms such that most of the theorems coming from the heart of mathematics are either provable within RCA 0 , or provably equivalent to one of these systems.
In this talk, we will introduce reverse mathematics with its motivations, and will give a glimpse of this computational structural phenomenon. Last, we will present the new problematics of modern reverse mathematics together with its main remaining open questions.
References
Hirschfeldt, D.R.: Slicing the truth, Lecture Notes Series. Institute for Mathematical Sciences. National University of Singapore, vol. 28. World Scientific Publishing Co. Pte. Ltd., Hackensack, NJ (2015), on the computable and reverse mathematics of combinatorial principles, Edited and with a foreword by Chitat Chong, Qi Feng, Theodore A. Slaman, W. Hugh Woodin and Yue Yang
Simpson, S.G.: Subsystems of Second Order Arithmetic. Cambridge University Press (2009)
