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:4938@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20231102T110000
DTEND;TZID=Europe/Paris:20231102T123000
DTSTAMP:20260107T154518Z
URL:https://www.i2m.univ-amu.fr/evenements/seminaire-lsc-matteo-acclavio-g
 ianluca-curzi/
SUMMARY:Matteo Acclavio\, Gianluca Curzi (U. of southern Denmark\, Gothenbu
 rg): Infinitary cut elimination via finite approximations
DESCRIPTION:Matteo Acclavio\, Gianluca Curzi: We investigate non-wellfounde
 d proof systems based on parsimonious logic\, a weaker variant of linear l
 ogic where the exponential modality ! is interpreted as a constructor for 
 streams over finite data. Logical consistency is maintained at a global le
 vel by adapting a standard progressing criterion. We present an infinitary
  version of cut-elimination based on finite approximations\, and we prove 
 that\, in presence of the progressing criterion\, it returns well-defined 
 non-wellfounded proofs at its limit. Furthermore\, we show that cut-elimin
 ation preserves the progressive criterion and various regularity condition
 s internalizing degrees of proof-theoretical uniformity. Finally\, we prov
 ide denotational semantics for our systems based on the relational model.\
 n\nThis is joint work with Giulio Guerrieri (Aix Marseille Université\, F
 rance)\n\nLieu : LIS\, salle REU 04.01
CATEGORIES:Séminaire,Logique et Interactions,LSC
LOCATION:Luminy\, Campus des Sciences de Luminy\, Marseille\, 13009\, Franc
 e
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=Campus des Sciences de Lumi
 ny\, Marseille\, 13009\, France;X-APPLE-RADIUS=100;X-TITLE=Luminy:geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20231029T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR