Programmation, simulations, topologie et types dépendants (and much more if time permits)


Pierre Hyvernat, Institut mathématique de Luminy. 19 janvier 2006 10:00 limd 2:00:00
Abstract:

En partant d'une structure généralisant les graphes de transitions et les simulations, je montrerai comment relier les notions de programmes (ceux de la vraie vie) et de fonctions continues (celles de la topologie constructive). Ceci donne un contenu concret à la 171 topologie formelle 187 de Giovanni Sambin et peut-être vu comme une extension de l'isomorphisme de Curry-Howard. De plus tous les résultats peuvent être développés dans la théorie des types dépendants 171 à la suédoise 187. Plus généralement, la notion utilisée permet de décrire tout phénomène interactif entre un utilisateur et son environnement. La structure résultante permet, entre autre, de donner un modèle non-trivial du lambda-calcul différentiel et semble ainsi relier deux visions des calculs de processus. (??)