Alberto Carraro
Università Ca' Foscari, Venise
https://independent.academia.edu/AlbertoCarraro
Date(s) : 16/01/2014 iCal
11 h 00 min - 11 h 30 min
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