Cette thèse porte sur les propriétés mathématiques du Calcul et, plus particulièrement, sur le déterminisme et la séquentialité. Dans une perspective issue de la théorie de la démonstration, elle porte aussi sur l’accès aux ressources, avec l’étude des exponentielles de la Logique Linéaire, ainsi que sur l’interactivité interne du Calcul, dont la Ludique de J.-Y. Girard tire par ailleurs parti.
Notre point de vue est celui de la sémantique dénotationnelle : nous modélisons le Calcul en interprétant ses (...)
Recherche
1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | 17 | 18 | 19 | 20 | 21 | 22 | 23 | 24 | 25 | 26 | 27 | 28 | 29 | 30 | 31 | 32
Mes travaux de recherche s’inscrivent en théorie de la démonstration dans le champ ouvert par Jean-Yves Girard, notamment par l’introduction de la logique linéaire.
Les travaux listés ici portent essentiellement sur l’étude de sémantiques dénotationnelles, en particulier les hypercohérences de Thomas Ehrhard et la sémantique des jeux.
Plus globalement, je m’intéresse :
aux propriétés mathématiques du calcul et à ce que l’interprétation mathématique des objets calculatoires permet de révéler sur la nature des preuves et des programmes,
à la programmation d’un point de vue théorique (notamment via l’isomorphisme de Curry-Howard) mais aussi pratique (en tant que programmeur régulier et enseignant). Et, dans le champs des sciences humaines, je m’intéresse à la programmation en tant que capacité humaine inédite et, plus largement, aux enjeux sociaux de l’informatique (en tant que passeur ayant démarré très jeune avec l’Apple II, puis le modem intégré du minitel et un fer à souder).
RSS 2.0
