Our site uses cookies necessary for its proper functioning. To improve your experience, other cookies may be used: you can choose to disable them. This can be changed at any time via the Cookies link at the bottom of the page.


Université de Bordeaux
Cluster SysNumCluster of Excellence
Cluster of excellence
 

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

le Thursday 14 February 2019 to 11h
Last update Friday 08 February 2019

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.

Picture in categories


TOP