A characterization of head-normalization through some intersection type systems and the relational model via Taylor expansion

Federico Olimpieri (Université d'Aix-Marseille)
06/10/2017 - 11:00
Dipartimento di Matematica e Fisica, L.go S. Leonardo Murialdo 1, Palazzina C, Aula 311

Via the Taylor expansion of lambda terms it is possible to provide an innovative proof of the head-normalization theorem for the relational model.
Thanks to this result we can also state in a very natural way the equivalence between the relational model and some intersection type systems.