For this first meeting of the new season of the GdT "Logique et Programmation" we will have Giulio Manzonetto (LIPN).
In this talk, we build a categorical model D of lambda calculus living in a category of sets and relations (relational semantics).
We will characterize the equational theory of this model, and show that it satisfies interesting algebraic properties that make it suitable for dealing with non-deterministic and parallel extensions of lambda calculus.
Unlike most traditional approaches, our way of interpreting non-determinism does not require any additional powerdomain construction: we show that our model provides a straightforward semantics of non-determinism (may convergence) by means of `unions' of interpretations as well as of `parallelism' (must convergence) by means of a binary, non-idempotent, operation available on the model, which is related to MIX rule of Linear Logic.
We describe the interpretation of this parallel and non-deterministic calculus in our model and show that this interpretation is sensible with respect to our operational semantics: a term converges if, and only if, it has a non-empty interpretation.
If time permits, we will sketch an interpretation of the resource lambda calculus in D.