Gilles DOWEK

Gilles Dowek

I am a researcher at Inria and professeur attaché at the ENS Paris-Saclay.

I am a member of the Laboratoire de Méthodes Formelles, in the Deducteam team where we develop the logical framework Dedukti and the encyclopedia Logipedia.

I am interested in the formalization of mathematics, in proof processing systems, in the physics of computation, in the safety of aerospace systems, and in the epistemology and ethics of informatics. Here is the list of my scientific papers and some books and philosophical papers.

I contribute to the Logique course in the third year of the bachelor degree. This is a flipped-classroom course, the videos are there. I contribute to the preparation of the Agrégation de mathématiques. I teach the course Foundations of proof systems at the MPRI. Here are its course notes Proofs in theories. Here are the videos of ten lectures of 1:30 each of the course the principles of programming languages I taught at École polytechnique.

Some of my course notes have been published, as books, others are on line.

I am a member of the of the Comité national pilote d'éthique du numérique, of the Conseil national du numérique, of the Scientific board of the Societé informatique de France of the Scientific board of La main à la pâte, and of the Comite national francais d'histoire et de philosophie des sciences et des techniques.

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 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 also have been 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 try to make science popular with books, videos, from may 2014 to june 2021, I wrote a monthly column in Pour la Science.

new Explanation: from ethics to logic at the CEA
new In Besançon: Les quatre concepts de l'informatique, Concevoir son propre langage de programmation
new An Ethical Turn in the Digital Industry?, I&E Talk
new Linear lambda-calculus is linear at the French-Argentinian Workshop on Logics and Dynamics of Programming Languages
new Postdoctoral position at Inria Saclay: B in Dedukti
new A short presentation of Dedukti and some questions to address, at the ICSPA kick-off meeting
new Civilisation numérique. Ouvrons le débat !
new Dictionnaire du numérique (in English soon)
new Pour une éthique du numérique
new Le Numérique at the Conseil d'État
new Linear lambda-calculus is linear
new Quelques orientations futures du numérique at the meeting IG / IA-IPR NSI
new A masters internship: Apprentissage automatique et traduction de démonstrations formelles, with Guillaume Lample
new A New connective in natural deduction, and its application to quantum computing at the Pontifícia Universidade Católica do Rio de Janeiro
new Ecumenism: logical constants and beyond at the Pontifícia Universidade Católica do Rio de Janeiro
new A masters internship: Propriétés formelles des interactions écologiques, with Cédric Gaucherel
new Sommes-nous plus libres parce que le monde va au hasard ?
new Sharing geometry proofs across logics and systems at the 13th International Conference on Automated Deduction in Geometry
new A. Díaz-Caro and G. Dowek, A New Connective in Natural Deduction, and its Application to Quantum Computing, 18th International Colloquium on Theoretical Aspects of Computing bpa Best paper award shared with Muhammad Hannan Khan, Osman Hasan, and Shahid Khan for their paper Accelerating SpMV Multiplication in Probabilistic Model Checkers using GPUs
new Interacting safely with an unsafe environment at Logical Frameworks and Meta-Languages.
new Explanation from ethics to logic (25 mn) at the Symposium Fairness, Integrity and Transparency of Formal Systems: Challenges for a Society Increasingly Dominated by Technology
new Douze leçons de logique
new F. Blanqui, G. Dowek, É. Grienenberger, G. Hondet, and F. Thiré, Some axioms for mathematics
new Les questions éthiques posées par l'intelligence artificielle (beware 1:22:29)

research papers, course notes, philosophy of sciences papers, books, videos

About LSV



Gilles DOWEK
LSV, CNRS & ENS Paris-Saclay
4, avenue des Sciences, CS 30008,
91192 Gif-sur-Yvette, France