Séminaires

Séminaire LoCaL

Historiquement, l'approche franco-italo-japonais de la logique linéaire accorde beaucoup d'importance à la notion de réseaux de preuve. Celle-ci est, à son tour, basée sur un ensemble d'objets de nature calculatoire (des espèces de programmes non-typés) que l'on peut appeler des "structure de preuve non-typées". Dans l'exposé, je considérerai par parti pris les processus du pi-calcul comme des structures de preuve non-typées et non-déterministes, et je montrerai comment arriver aux réseaux de preuve d'une version de la logique linéaire avec cocontraction (mais sans coaffaiblissement ou codéreliction). S'il y a le temps, je parlerai de comment libéraliser cela pour obtenir un système de types pour le pi-calcul garnatissant l'absence de deadlock tout en permettant des processus "cycliques", habituellement exclus des systèmes de type à base de logique linéaire. Ceci est un travail en collaboration avec Juan Jaramillo et Jorge Perez (Université de Groeningen).

Réunion de plannification