Matteo Acclavio / Gianluca Curzi
University of Southern Denmark / University of Gothenburg, Sweden
Date(s) : 02/11/2023 iCal
11 h 00 min - 12 h 30 min
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
Campus de Luminy, Marseille
Catégories