Évènement

Alberto Carraro
Università Ca' Foscari, Venise
https://independent.academia.edu/AlbertoCarraro

Date(s) : 16/01/2014   iCal
11h00 - 11h30

We present some results about the relational semantics of λ-calculus. The standard relational semantics satisfies the so-called Taylor expansion formula and this forces all models of untyped λ-calculus in it to be sensible. We illustrate a model, obtained by modifying the exponential modality, in which the Taylor formula does not hold, allowing the existence of a non-sensible relational model. For a model in the standard semantics we illustrate a syntax in which all points are definable, leading to a full abstraction result. We then move our attention to call-by-value λ-calculus in the relational semantics. We characterize the solvable terms and we discuss the relationship between the equational theory of a model, Böhm trees, and operational equivalence. We will point out how all the ideas underlying these results come from (Differential) Linear Logic.

https://www.dsi.unive.it/~acarraro/

Catégories

• Séminaire