Essential and relational models

What is it about?

The paper is about models of the untyped lambda calculus. The relational models gives rise lambda-algebras that become lambda-models by means of a suitable tricks. We explored this trick under Stone-duality, namely in the setting of logical models built on intersection types. We show that a non-standard interpretation allows us to pick up the family of essential models that exactly correspond to strongly-linear relational models.

Featured Image

Why is it important?

Since it extends the standard interpretation provided for logical models and it provides a finitary language for the analysis of programs under the relational equivalence.

Perspectives