Welcome to Gilles DOWEK's home page


I am a researcher at Inria in the Deducteam team and in the Mooc Lab.

I am interested in the formalization of mathematics (type theory, set theory, nominal logics, etc.), in proof processing systems (proof-checking, automated theorem proving, etc.), in the design of quantum programming languages and in the safety of aerospace systems. Here is the list of my publications.

I am a member of the Scientific board of the Societé informatique de France and of the CERNA, Commission de réflexion sur l'éthique de la recherche en sciences et technologies du numérique d'Allistene, l'Alliance des sciences et technologies du numérique. In the past, I have been Deputy Scientific Director of Inria in charge of the domain Algorithmic, Programming, Software and Architectures.

I am also a consultant for the National Institute of Aerospace, a lab of the NASA Langley research center. Among other things, I have participated to the development and the proof of ACCoRD, an Airborne Coordinated Conflict Resolution and Detection system.

I teach the course Foundations of proof systems at the MPRI, here is the page of my course and its course notes Proofs in theories. More generally, I am interested in education and I try to draw the attention of the adminstration to the need of introducing computer science in K-12. I am a member of the joint ITIC group of the Société Informatique de France and the organization Enseignement public & informatique. I have been a member of the Committee apointed by the Minister of Education to suggest a computer science curiculum for senior high school students, this has lead to the curiculum published in the Bulletin officiel on October 13th 2011. I have participated to the report of the Academy of Sciences L'enseignement de l'informatique - Il est urgent de ne plus attendre. I am a member of the Scientific board of La main à la pâte. I have participated to the creation of the blog of the Committee on European Computing Education. I have previously been a professor in l'École polytechnique. Here are my course notes and the videos of ten lectures of 1:30 each on the principles of programming languages.

I write popular science, in particular I write a monthly chronicle in Pour la Science.

Finally, I am interested in the philosophy of sciences.

new Happy birthday Luiz Carlos: Why is this a Proof?
new The slides of my talk at IFIP WG 1.6: Polarization and Reachability.
new The slides of my talk at Tools for teaching logic: Rules and derivations in an elementary logic course.
new Écrire et se repentir
new G. Burel, G. Dowek, and Y. Jiang, A completion method to decide reachability in rewrite systems.
new Computation Proof Machine Computation Proof Machine: mathematics enters a new age has been published
newThe blog of the Committee on European Computing Education
To contact me:
(my first name).(my last name)
Inria, 23 avenue d'Italie, CS 81321, 75214 Paris Cedex 13, France.
+ 33 1 39 63 57 10
research papers, course notes, philosophy of sciences, popular science