BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:5979@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20220908T110000
DTEND;TZID=Europe/Paris:20220908T123000
DTSTAMP:20241120T200709Z
URL:https://www.i2m.univ-amu.fr/evenements/why-are-proofs-relevant-in-proo
 f-relevant-models/
SUMMARY:Axel Kerinec (LIPN\, Université Sorbonne Paris Nord): Why Are Proo
 fs Relevant in Proof-Relevant Models?
DESCRIPTION:Axel Kerinec: Relational models of 𝜆-calculus can be present
 ed as type systems\, the relational interpretation of a 𝜆-term being gi
 ven by the set of its typings. Within a distributors-induced bicategorical
  semantics generalizing the relational one\, we identify the class of ‘c
 ategorified’ graph models and show that they can be presented as type sy
 stems as well. We prove that all the models living in this class satisfy a
 n Approximation Theorem stating that the interpretation of a program corre
 sponds to the filtered colimit of the denotations of its approximants.\nAs
  in the relational case\, the quantitative nature of our models allows to 
 prove this property via a simple induction\, rather than using impredicati
 ve techniques. Unlike relational models\, our 2-dimensional graph models a
 re also proof-relevant in the sense that the interpretation of a 𝜆-term
  does not contain only its typings\, but the whole type derivations. The a
 dditional information carried by a type derivation permits to reconstruct 
 an approximant having the same type in the same environment. From this\, w
 e obtain the characterization of the theory induced by the categorified gr
 aph models as a simple corollary of the Approximation Theorem: two 𝜆-te
 rms have an isomorphic interpretation exactly when their Böhm trees coinc
 ide.
CATEGORIES:Séminaire,Logique et Interactions
LOCATION:I2M Luminy - Ancienne BU\, Salle Séminaire2 (RdC)\, 163 Avenue de
  Luminy\, 13009 Marseille\, France\, 
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=163 Avenue de Luminy\, 1300
 9 Marseille\, France\, ;X-APPLE-RADIUS=100;X-TITLE=I2M Luminy - Ancienne B
 U\, Salle Séminaire2 (RdC):geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20220327T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR