Séminaire LSC : Matteo Acclavio / Gianluca Curzi, Infinitary cut elimination via finite approximations
Date(s) : 02/11/2023 iCal
11h00 - 12h30
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level 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-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide denotational semantics for our systems based on the relational model.
This is joint work with Giulio Guerrieri (Aix Marseille Université, France)
Lieu : LIS, salle REU 04.01
Emplacement
Luminy
Catégories
