Institut de Mathématiques de Marseille

SÉMINAIRES 2014
Logique et Interactions

Organisateur :
Emmanuel Beffara (tél. 04 91 26 96 35)
Lieu : IML, Bâtiment TPR2- CNRS :
Salle de Séminaires : 3ème étage (304-306).
Horaire : en règle générale le jeudi, à 14h.

du lundi 10 au vendredi 14 février

Giuseppe Greco

Giuseppe Greco
(Delft University of Technology) :
Proof theory for dynamic logics

Webpage : http://tudelft.academia.edu/GiuseppeGreco

Abstract: We introduce a multi-type display calculus for (intuitionistic) dynamic epistemic logic and (concurrent) propositional dynamic logic, which we refer to as Dynamic Calculi. The display approach is suitable to modularly chart the space of dynamic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculi with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems that enjoy a generalisation of the Curry-Belnap cut-elimination meta-theorem.


jeudi 30 janvier

à 14h
Pierre Boudes

Pierre Boudes
(LIPN, Paris 13) :
À préciser

Webpage : http://lipn.univ-paris13.fr/~boudes/


jeudi 16 janvier

à 14h
Alberto Carraro

Alberto Carraro
(Università Ca' Foscari, Venise) :
Semantical analysis of λ-calculus
by (Differential) Linear Logic

Webpage : http://www.dsi.unive.it/~acarraro/

Abstract: 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.

 

Liste des séminaires de l'année ...
[2002] [2003] [2004] [2005] [2006] [2007] [2008] [2009] [2010] [2011] [2012] [2013]

EL, le 24 janvier 2014