Vendredi 22 Avril

Retour à la vue des calendrier
Vendredi 22 Avril
Heure: 11:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: New Results on Morris's Observational Theory: the benefits of separating the inseparable
Description: Giulio Manzonetto We study the theory of contextual equivalence in the untyped lambda-calculus, generated by taking the normal forms as observables. Introduced by Morris in 1968, this is the original extensional lambda theory H+ of observational equivalence.
On the syntactic side, we show that this lambda-theory validates the omega-rule, thus settling a long-standing open problem. On the semantic side, we provide sufficient and necessary conditions for relational graph models to be fully abstract for H+. We show that a relational graph model captures Morris's observational pre-order exactly when it is extensional and lambda-König. Intuitively, a model is lambda-König when every lambda-definable tree has an infinite path which is witnessed by some element of the model.
Joint work with Flavien Breuvart, Domenico Ruoppolo & Andrew Polonsky