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

Nous avons le grand plaisir de vous inviter au colloque “Formalization of proofs, formalization of programs”, qui se tiendra les 18 et 19 Décembre à 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.

Le colloque explorera les relations, ou leur absence, entre deux champs de recherche fondamentale : l’informatique et les mathématiques. Alors que le calcul appartenait auparavant au champ disciplinaire des mathématiques, ce n’est clairement plus le cas aujourd’hui, et il est donc fondamental de repenser les relations possibles entre ces deux champs. Le but de colloque est de réexaminer les concepts et pratiques de la formalisation, la programmation et du calcul dans ces deux contextes.

Pour vous inscrire, merci d’envoyer un courriel à maelpegny@gmail.com avant le 13 décembre 2019. L’inscription est gratuite mais nécessaire.

Le colloque a été le fruit de la collaboration de deux projets de recherche, le projet ANR-DFG FFIUM et le projet ANR PROGRAMme.

Organisateurs : Liesbeth De Mol (PROGRAMme), Alberto Naibo, Marco Panza, Gerhard Heinzmann (FFIUM), Maël Pégny (OLKi).

Les titres et résumés des exposés sont disponible ici.

PROGRAMME PROVISOIRE

Mercredi 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: 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: Table Ronde “What can be formalized?” Contributions de: 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: 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 sciences: formal methods for all?