workshop Formalization of proof, Formalization of programs, 18-19 december 2019, Paris

*Workshop announcement*

FORMALIZATION OF PROOFS, FORMALIZATION OF PROGRAMS,

Paris, December, 18-19 2019

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.

https://programme.hypotheses.org/ffium-programme-colloquium-formalization-of-proofs-formalization-of-programs

*Mercredi 18 décembre 2019*

9h30-10h45: Ursula Martin, What can studies of crowdsourcing tell us about mathematical practice?

10h45-11h: Coffe Break

11h-12h15: Gilles Dowek: The absoluity of logical truth challenged by proof formalization.

12h15- 14h00: Lunch

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: Coffe Break

16h45-18h30: Table Ronde “What can be formalized?” with contributions from: Simone Martini, Baptiste Mélès, Maël Pégny, Maté Szabo

*Jeudi 19 décembre 2019*

9h30-10h45: Cliff Jones, Formalisation and Proof in Computing: A Personal View

10h45-11h00: Coffe Break

11h00-12h15: Assia Mahboubi, Verified Computations in Mathematical Proofs

12h15- 14h00: Lunch

14h00-15h15: Giuseppe Primiero, Value-sensitive co-design for resilient software systems

15h15-15h30: Coffe Break

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?

The workshop intends to reconsider the relations or lack thereof between 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 this makes urgent to rethink the possible relations between the two fields. The workshop aim to do it by studying notions and practices of formalization 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 workshop results from a collaboration between two ANR research projects:
the FFIUM Project (https://sites.google.com/view/ffium/accueil)
and the PROGRAMme project (https://programme.hypotheses.org/).

Organizors: Liesbeth De Mol, Gerhard Heinzmann, Alberto Naibo, Marco Panza.