Séminaire Logique et Interactions
Le séminaire Logique et Interaction est le séminaire de l’équipe LDP de l’I2M. Il est conjoint au séminaire de l’équipe LSC du LIS.
Une liste de diffusion (modérée) pour recevoir les annonces d’exposés : i2m-seminaire-logique@univ-amu.fr
Pour s’inscrire, contacter le responsable.
Les prochains séminaires
21
May
28
May
25
Jun
02
Jul
Événements passés
28
May
Treillis et extensions de la logique linéaire additive
Olivier Laurent (LIP, CNRS, ENS Lyon)
Certaines structures ordonnées libres peuvent être représentées à l'aide de la relation de déduction du calcul des séquents. En particulier, Withman a montré par anticipation [...]
Représentation des fonctions continues entre "streams" (& Co.) par des types de données
Pierre Hyvernat (LAMA, Université Savoie Mont Blanc)
Brouwer savait déjà que les fonctions continues entre streams (avec la topologie produit habituelle) pouvaient être représentées par des arbres infinis. Peter Hancock a montré [...]
Bar recursion, sémantique dénotationnelle et réalisabilité classique
Jean-Louis Krivine (PPS, Université Paris-Diderot)
L'opérateur de bar recursion, introduit dans les années 60 par C. Spector pour "prouver" la consistance de l'Analyse, a été recyclé à partir de 1998, [...]
Types inductifs stricts et paresseux, du point de vue de la logique linéaire
Thomas Ehrhard (PPS, Université Paris-Diderot)
TBA http://www.pps.univ-paris-diderot.fr/~ehrhard/
A semantic study of higher-order model-checking
Charles Grellois (LIS, LIRICA team, Aix-Marseille Université)
Using higher-order recusion schemes, one can model the computation flow of functional programs, and produce trees abstracting their set of executions. The higher-order model-checking problem [...]
Topologies faibles et logique linéaire
Marie Kerjean (PPS, Université Paris-Diderot)
Je présenterai dans cet exposé un modèle de la logique linéaire différentielle où les formules sont interprétées par les espaces vectoriels topologiques localement convexes. La [...]
09
Oct
02
Oct
Programmation logique, unification et espace logarithmique
Clément Aubert (I2M, Aix-Marseille Université)
Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance [...]
