Domenico Ruoppolo
LIPN, Université Paris 13
https://www.doc.ic.ac.uk/~druoppol/
Date(s) : 16/03/2017 iCal
11 h 00 min - 12 h 00 min
On présente les modèles de graphes relationnels (rgm), une sous-classe des modèles relationnels du lambda-calcul pur (les objects réflexifs dans la catégorie cartésienne fermée MRel engendrée par la sémantique relationnelle de LL). Les rgm sont une version relationnelle à la fois des modèles de graphes et des modèles filtres.
Nous nous servons des rgm pour obtenir la full abstraction (adéquation complète) par rapport à deux différentes théories observationnelles : celle qui considère les formes normales de tête comme termes observables (connu sous le nom de théorie H) et celle qui prend les formes beta-normales comme observables (théories de Morris). Non seulement nous trouvons des modèles fully abstract, mais nous donnons une solution exhaustive au problème, en caractérisant tout rgm ayant la théorie H ou la théorie de Morris. Les deux théories sont caractérisées par deux notions duales, données en termes de types intersection non-idempotents.
(joint work with Flavien Breuvart, Giulio Manzonetto and Andrew Polonsky)
Catégories