Groupe de travail Pôle Preuves, programmes et systèmes Équipe thématique Preuves et programmes Gestion des séances Preuves, programmes et tout ça Jour, heure et lieu Le jeudi à 14h, salle 1007 Le calendrier des séances (format iCal). Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien. Contact(s) Delia Kesner Prochaine séance Preuves, programmes et tout ça Jeudi 30 mars 2023, 13 heures 30, salle 4052 Nino Salibra (Universita' Ca'Foscari Venezia) A completeness theorem for the infinitary lambda calculus Séances passées Année 2023 Preuves, programmes et tout ça Mardi 28 mars 2023, 13 heures 30, salle 3052 Fabio Massaioli (Scuola Normale Di Pisa) (Scuola Normale di Pisa) A non-trivial proof-semantics for classical sequent calculus (LK) Cut-reduction procedures for classical sequent calculus are notoriously non-deterministic and non-confluent, both in the original formulation by Gentzen and in later reformulations. It is natural to ask whether those instances of non-confluence are superficial in nature, i.e. whether syntactically distinct normal forms of the same derivation are in fact correlated in a non-trivial way, as is the case in the intuitionistic and linear versions of sequent calculus. A famous counter-example by Lafont purports to show that the answer is negative, that is, every interpretation of derivations in LK that is invariant under classical cut-elimination must be a trivial one that identifies at least all proofs of the same sequent. A long-standing open question has then been whether it could be possible to work around Lafont's example by natural and non-trivial adjustments of the calculus and/or of cut-reduction steps, without resorting to symmetry-breaking techniques like polarization or embeddings into intuitionistic or linear logic. Working within the propositional fragment of the context-sharing formulation of LK — where parallel logical rules permute freely — we show that the graph constructed by tracing the history of atomic formula occurrences through axiom and cut rules is invariant under arbitrary rule permutations in cut-free proofs, thus providing a canonical representation of normal-form proofs. We then introduce a refinement of the notion of axiom-induced graph that allows extending the invariance result to proofs with cuts, although at the cost of a strong assumption on the shape of derivations. Because cut-reduction in this formulation of LK can be implemented entirely by logical rule permutations plus a pair of local rewriting steps that preserve the refined axiom graphs, the result yields a non-trivial invariant of cut-reduction. Preuves, programmes et tout ça Jeudi 9 mars 2023, 14 heures, salle 1007 Daniele Pautasso (Univ. Torino) A quantitative version of simple types Our work introduces a quantitative version of the simple type assignment system, starting from a suitable restriction of non-idempotent intersection types. The key idea is to restrict multiset formation to uniform types, two types being uniform if they differ only in the cardinality of the multisets occurring in it. The resulting system has the same typability power as the simple type assignment system; thus, assigning types to terms supplies the very same qualitative information given by simple types, but at the same time provides some interesting quantitative information. It is well known that typability for simple types is equivalent to unification; we prove a similar result for the newly introduced system. More precisely, we show that typability is equivalent to a unification problem which is a non-trivial extension of the classical one: in addition to unification rules, our typing algorithm makes use of an operation that increases the cardinality of multisets whenever needed. Preuves, programmes et tout ça Jeudi 2 mars 2023, 14 heures, salle 1007 Riccardo Treglia Intersecting effects: two orthogonal approaches Preuves, programmes et tout ça Jeudi 9 février 2023, 14 heures, salle 1007 Giovanni Bernardi Breaking circles Preuves, programmes et tout ça Jeudi 26 janvier 2023, 14 heures, salle 1007 Sandra Alves Quantitative Weak Linearisation Année 2022 Preuves, programmes et tout ça Jeudi 15 décembre 2022, 14 heures, salle 1007 Victor Arrial Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework Preuves, programmes et tout ça Jeudi 3 novembre 2022, 14 heures, salle 1007 Loic Peyrot Repetition soutenance de these Preuves, programmes et tout ça Vendredi 28 octobre 2022, 14 heures, salle 1007 Pablo Barenbaum Proof Terms for Higher-Order Rewriting and Their Equivalence Preuves, programmes et tout ça Mercredi 19 octobre 2022, 14 heures, salle 1007 Adrienne Lancelot Open Call-by-Value and Open Similarity