FFIUM/PROGRAMme colloquium: formalization of proofs, formalization of programs

Une version francaise est disponible ici.

It is with great pleasure that we invite you to the colloquium on “Formalization of proofs, formalization of programs” to be held from 18-19 december in Paris Paris Campus Lourcine, 1, rue de la Glacière (RER : Port Royal; Metro, ligne 7 : Les Gobelins; Metro, ligne 6 : Glacière). Bâtiment 2, Salle 02-Gérard Lyon-Caen.

The colloquium intends to explore the relations or lack thereof between two basic fields: Computer science and mathematics. Whereas, originally, mathematics was used to provide a disciplinary identity to computing, today, this is clearly no longer the case and so it is basic to rethink the possible relations (epistemological or other) between the two fields. The aim of this workshop is to reconsider the relations between computing and mathematics by studying notions and practices of formalization, programming and computation in both contexts.

In order to register, please send a mail to maelpegny@gmail.com before 13 december 2019. Registration is free but necessary.

The colloquium is the result of a collaboration between two ANR research projects, the ANR FFIUM Project (https://sites.google.com/view/ffium/accueil) and the ANR PROGRAMme project (https://programme.hypotheses.org/).

Organizors: Liesbeth De Mol, Gerhard Heinzmann, Alberto Naibo, Marco Panza, Maël Pégny.

Titles and abstracts are available here.


Wednesday 18 décembre 2019:
9h30-10h45: Ursula Martin, What can studies of  crowdsourcing tell us about mathematical practice?
10h45-11h: Pause
11h-12h15: Gilles Dowek: L’absoluité de la vérité logique à l’épreuve de la formalisation des démonstrations./ The absoluity of logical truth challenged by proof formalization.
12h15- 14h00: déjeuner
14h00-15h15: Gisele Secco, Diagrams and Programs in the First Proof of the Four-Color Theorem
15h15-16h30: Raymond Turner, Some Instances of Abstraction in Mathematics and Computer Science
16h30-16h45: Pause
16h45-18h30: Roundtable “What can be formalized?” with contributions from: Simone Martini, Baptiste Mélès, Maël Pégny, Maté Szabo

Thursday 19 décembre 2019:
9h30-10h45: Cliff Jones, Formalisation and Proof in Computing: A Personal View
10h45-11h00: Pause
11h00-12h15: Giuseppe Primiero, Value-sensitive co-design for resilient software systems
12h15- 14h00: déjeuner
14h00-15h15: Assia Mahboubi, Verified Computations in Mathematical Proofs
15h15-15h30: Pause
15h30-16h45: Alberto Naibo, Formalizing constructions and proofs in Euclid’s geometry
16h45-18h: Cyrille Imbert, Vincent Ardourel, Program verification in the empirical science: formal methods for all?