Séminaire Logique et Interactions
Le séminaire Logique et Interaction est le séminaire de l’équipe LDP de l’I2M. Il est conjoint au séminaire de l’équipe LSC du LIS.
Une liste de diffusion (modérée) pour recevoir les annonces d’exposés : i2m-seminaire-logique@univ-amu.fr
Pour s’inscrire, contacter le responsable.
Les prochains séminaires
12
Fév
Is typed realizability only predicative?
Félix Castro (I2M, Aix-Marseille)
In Kleene realizability, formulas are interpreted as sets of (untyped) programs. This approach allows for a sound interpretation of Higher-Order Logic (HOL): it leads to [...]
19
Fév
Ohana trees, Taylor expansion and multi-type semantics for the λI-calculus. No variable gets left behind or forgotten!
Rémy Cerda (Università di Bologna)
The standard notion of evaluation trees for the λ-calculus, namely Böhm trees, is quite ill-behaved with respect to the inputs of programs, namely free variables: [...]
Événements passés
Coordinatizing MV algebras and AF C*-algebras by inverse monoids
Philip Scott (University of Ottawa)
Slides Joint work with M. Lawson.
Canonicity of groupoids laws using parametricity theory
Marc Lasson (University of Cambridge)
The synthetic approach to weak ω-groupoids promoted by the univalent foundation program is the idea that (homotopy) type theory should be the primitive language in [...]
Type theory modulo isomorphisms
Alejandro Díaz-Caro (INRIA Rocquencourt & Paris Ouest)
We defined a typed lambda-calculus where the isomorphisms between types are raised to the level of an equality relation. To this end, an equivalence relation [...]
Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi
Benoît Valiron (PPS, Université Paris-Diderot)
In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model model of linear logic. We first define [...]
Category theory in the Univalent Foundations
Benedikt Ahrens (CIMI, University Paul Sabatier, Toulouse)
The Univalent Foundations is an extension of Intensional Martin-Löf Type Theory (MLTT) recently proposed by V. Voevodsky. Its novelty is the Univalence Axiom which implements [...]
Proof theory for dynamic logics
Giuseppe Greco (Delft University of Technology)
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 [...]
Une analyse philosophique et quelques résultats sur le typage
Paolo Pistone (I2M, Aix-Marseille Université)
TBA
La réduction dans le λ-calcul avec ressources
Jean-Baptiste Midez (I2M, Aix-Marseille Université)
TBA
Semantical analysis of λ-calculus by (Differential) Linear Logic
Alberto Carraro (Università Ca' Foscari, Venise)
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 [...]
