Groupe de travail Pôle Preuves, programmes et systèmes Équipe thématique Preuves et programmes Gestion des séances La syntaxe rencontre la sémantique 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 Subscribe to the list gdt-sms@listes.irif.fr to receive announcements concerning this working work. Prochaines séances La syntaxe rencontre la sémantique Jeudi 21 décembre 2023, 14 heures, Salle 1007 Gabriel Scherer (INRIA) Constructor unboxing In this work I will present a new feature proposed for the OCaml programming language, “constructor unboxing”, first suggested by Jeremy Yallop in March 2020. It enables a more efficient representation of certain sum types, but requires a static analysis to forbid certain unboxing requests that would be unsound. To define this static analysis, one has to solve a problem of normalization of first-order definitions in presence of recursion. In the talk I hope to explain my current understanding of this halting problem, and present an algorithm to compute normal forms and reject (in finite time) non-normalizable definitions. La syntaxe rencontre la sémantique Jeudi 18 janvier 2024, 15 heures, Salle 1007 Jui-Hsuan Wu (LIX, Polytechnique) Proofs as Terms, Terms as Graphs La syntaxe rencontre la sémantique Jeudi 25 janvier 2024, 14 heures, Visio Davide Catta (Università degli Studi di Napoli Federico II) Game semantics and a new lambda calculus for the constructive modal logic CK Constructive modal logics are extensions of intuitionistic logic obtained by adding unary operators, called modalities, to the language of intuitionistic logic. These logics have generated increasing interest over the past decades, being investigated from both proof theory and type theory perspectives. In this talk, we investigate the Curry-Howard correspondence for constructive modal logic CK in light of the gap between the proof equivalences enforced by the lambda calculi from the literature and by the recently defined winning strategies for this logic. We present a game semantics for CK and a new lambda-calculus system for this logic, obtained by enriching the calculus from the literature with additional reduction rules. We then provide a typing system in the style of focused proof systems, allowing us to provide a unique proof for each term in normal form. Finally, we use this result to show a one-to-one correspondence between terms in normal form and winning innocent strategies for CK. (Joint work with Matteo Acclavio and Federico Olimpieri). Séances passées Année 2023 La syntaxe rencontre la sémantique Jeudi 7 décembre 2023, 14 heures, Salle 3052 Pablo Barenbaum (Universidad Buenos Aires) Sharing in linear logic and call-by-need La syntaxe rencontre la sémantique Jeudi 26 octobre 2023, 14 heures, salle 1007 Giuseppe Castagna (IRIF, CNRS and Univ. Paris Cite) A type system for Elixir La syntaxe rencontre la sémantique Jeudi 12 octobre 2023, 14 heures, salle 3052 Mariana Milicich (Université Paris Cité, CNRS, IRIF) Useful Evaluation, Inductively and Quantitatively Is λ-calculus a reasonable machine according to Van Emde Boas' Invariance Thesis? By defining the useful evaluation strategy, B. Accattoli and U. Dal Lago were able to answer positively to this question. However, their characterization doesn't facilitate the use of inductive arguments to reason about it. And, up to this date, there are no quantitative models to capture its time complexity. In this talk I'll discuss the first inductive characterization of the useful evaluation for open call-by-value. We achieve this by parameterizing the evaluation relation with respect to the information provided by the context in which the computation takes place. First we prove some properties of our notion of useful calculus. Then, we give a quantitative model for the useful strategy, using a non-idempotent intersection type system with tight rules. Therefore, typing a term t gives exact information about how many steps does the computation requires to compute the normal form of t. La syntaxe rencontre la sémantique Jeudi 28 septembre 2023, 14 heures, Salle 3052 Beniamino Accattoli (INRIA Saclay) Closure Conversion and Abstract Machines Closure conversion is a program transformation at work in compilers for functional languages to turn inner functions into global ones, by building 'closures' pairing the transformed functions with the 'environment' of their free variables. Abstract machines rely on similar and yet different concepts of 'closures' and 'environments'. In this talk, we analyze the relationship between the two approaches. We adopt a very simple lambda-calculus with tuples as source language and study abstract machines for both the source language and the target of closure conversion. We overview three contributions. Firstly, a new simple proof technique for the correctness of closure conversion, inspired by abstract machines. Secondly, we show how the closure invariants of the target language allow us to design a new way of handling environments in abstract machines, not suffering the shortcomings of other styles. Thirdly, we analyze the machines from the point of view of sharing and time complexity, dissecting how different aspects of closure conversion impact on the cost of the execution. La syntaxe rencontre la sémantique Jeudi 22 juin 2023, 14 heures, salle 146 (Olympe de Gouges) Miguel Ramos (Univ. Porto) Quantitative CBV Global Memory La syntaxe rencontre la sémantique Jeudi 1 juin 2023, 14 heures, salle 146 (Olympe de Gouges) Gabriele Vanoni (Univ. Bologna) Higher-Order and Non-Linear Bayesian Networks La syntaxe rencontre la sémantique Mercredi 24 mai 2023, 14 heures, salle 147 (Olympe de Gouges) Jose Espirito Santo (Univ. Minho (Portugal)) The logical essence of compiling with continuations La syntaxe rencontre la sémantique Jeudi 20 avril 2023, 13 heures 30, salle 147 (Olympe de Gouges) Hugo Herbelin (IRIF, INRIA, Univ. Paris Cite) Under syntax and semantics, the logic La syntaxe rencontre la sémantique Jeudi 30 mars 2023, 13 heures 30, salle 4052 Nino Salibra (Universita' Ca'Foscari Venezia) A completeness theorem for the infinitary lambda calculus La syntaxe rencontre la sémantique 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. La syntaxe rencontre la sémantique 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. La syntaxe rencontre la sémantique Jeudi 2 mars 2023, 14 heures, salle 1007 Riccardo Treglia Intersecting effects: two orthogonal approaches La syntaxe rencontre la sémantique Jeudi 9 février 2023, 14 heures, salle 1007 Giovanni Bernardi Breaking circles La syntaxe rencontre la sémantique Jeudi 26 janvier 2023, 14 heures, salle 1007 Sandra Alves Quantitative Weak Linearisation La syntaxe rencontre la sémantique Jeudi 12 janvier 2023, 14 heures, salle 1007 Les Doctorants Du Groupe De Travail (Universite Paris Cite) Présentation des doctorants du groupe et de leur thématique de recherche Année 2022 La syntaxe rencontre la sémantique Jeudi 15 décembre 2022, 14 heures, salle 1007 Victor Arrial Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework La syntaxe rencontre la sémantique Jeudi 3 novembre 2022, 14 heures, salle 1007 Loic Peyrot Repetition soutenance de these La syntaxe rencontre la sémantique Vendredi 28 octobre 2022, 14 heures, salle 1007 Pablo Barenbaum Proof Terms for Higher-Order Rewriting and Their Equivalence La syntaxe rencontre la sémantique Mercredi 19 octobre 2022, 14 heures, salle 1007 Adrienne Lancelot Open Call-by-Value and Open Similarity