SysNum Seminar WP1-WP2 - David Janin, Université de Bordeaux - jeudi 14 janvier 11h IMB (A33) - salle 385

Séminaire Sysnum  WP1-WP2

David Janin (Université de Bordeaux)

Programs and proofs

Jeudi 14 février à 11h au A33 (IMB) - salle 385

Abstract
Dans cet exposé, destiné à un public très large, je donnerais de façon progressive et avec des exemples les notions clés qui permettent de voir les preuves comme des programmes, ouvrant ainsi la porte à la conception d’assistants de preuves, ou, de façon équivalente,  la conception d’assistants à la programmation correcte par construction. Cette exposé est aussi un apéritif à un cours de l’EDMI que je donnerais tous les lundi après-midi du mois de mars sur le langage de programmes/preuves Agda.