Recherche en logique linéaire

J’ai soutenu une thèse de doctorat là-dessus, cf. ma page professionnelle. (Il y a aussi de vrais bouts d’automates dedans.)

Vulgarisation sur la théorie de la démonstration

Articles dans la version livre du Tangente Hors-Série 55, « Les démonstrations », écrits avec Jérémy Ledent :

• « Une preuve de maths est un programme informatique ! », sur la correspondance de Curry-Howard ;
• « La théorie des types homotopique : de nouveaux fondements des mathématiques ? » sur la révolution en marche ;
• Un brouillon non publié sur la démonstration automatique, une version abrégée est parue.

Cours de logique au MPRI

Une ébauche de notes de cours de logique linéaire (MPRI 2-1). (Extrêmement incomplètes, vous feriez mieux de regarder le cours d’Olivier Laurent ou d’aller voir le Linear Logic Primer (en anglais) de V. Danos et R. di Cosmo.)

Ma présentation (tex) de l’article Control categories and duality de Peter Selinger, pour le cours de sémantique catégorique de Paul-André Melliès.

Logique épistémique

Ce n’est pas de la logique « sérieuse », voir à ce propos l’article Prisoners dans le dictionnaire de la logique dans Locus Solum (page 147). Cependant ça reste très amusant.

TODO : remplir cette section.