## Syntax Meets Semantics

#### Day, hour and place

Thursday at 2pm, room 1007

The calendar of events (iCal format).

In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link.

#### Contact(s)

Subscribe to the list gdt-sms@listes.irif.fr to receive announcements concerning this working work.

### Next talks

Syntax Meets Semantics

Thursday June 6, 2024, 2PM, Salle 3071

**Adrienne Lancelot** (LIX Polytechnique and IRIF UPC) *Mirroring Call-by-Need, or Values Acting Silly*

We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need – that is, its operational equivalence with call-by-name – showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.

Syntax Meets Semantics

Thursday June 20, 2024, 2PM, Salle 1020

**Victor Arrial** (IRIF, Universite Paris Cite) *The Benefits of Diligence*

### Previous talks

#### Year 2024

Syntax Meets Semantics

Thursday May 2, 2024, 2PM, Salle 3071

**Mariana Milicich** (IRIF, Universite Paris Cite) *Hybrid Intersection Types for PCF*

Syntax Meets Semantics

Thursday March 28, 2024, 2PM, Salle 3052

**Noam Zeilberger** (LIX, Polytechnique) *An introduction to type refinement systems*

Syntax Meets Semantics

Thursday February 15, 2024, 2PM, Salle 3052

**Hector Suzanne** (LIP6) *Une machine abstraite Call-By-Push-Value pour l'analyse de ressource*

La machine est une extension de la machine ILL_rho^eta de Curien et al.[1] avec des points fixes et une dépendance des types sur des paramètres de structures (taille, longueur, coût) qui sont contraints par une formule du premier ordre. Une phase de réécriture systématique, de et vers la machine, enrichit les programmes et définitions d'ADT avec des annotations de paramètres, de passage d'état et des primitives de coût. Elle implémente AARA comme un effet qui produit à la compilation une approximation sûre des manipulations de ressources à l'exécution.

Nous présentons l'exemple d'un miniML en appel par valeur des avec blocs monadiques et transformeurs de monades pour l'état mutable et les exceptions locales. L'analyse AARA demeure inchangée grâce aux implémentations canoniques des primitives monadiques dans CBPV. Une procédure de typage basée sur HM(X) a été implémentée et génère une contrainte globale sur les paramètres du programme entiers. Dans le cas classique où les coûts sont représentés par les polynômes en plusieurs variables, une procédure d'élimination des quantificateurs permet de se ramener à la programmation entière pour instancier des bornes explicites via un solveur externe.

Cet exposé reprend en grande partie le travail qui a été présenté à la conférence LOPSTR 2023 [2]

[1] doi.org/10.1145/2837614.2837652 [2] doi.org/10.1007/978-3-031-45784-5_5

Syntax Meets Semantics

Thursday January 25, 2024, 2PM, Visio

**Davide Catta** (Università degli Studi di Napoli Federico II) *Game semantics and a new lambda calculus for the constructive modal logic CK*

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).

Syntax Meets Semantics

Thursday January 18, 2024, 3PM, Salle 1007

**Jui-Hsuan Wu** (LIX, Polytechnique) *Proofs as terms, positively*

#### Year 2023

Syntax Meets Semantics

Thursday December 21, 2023, 2PM, Salle 3052

**Gabriel Scherer** (INRIA) *Constructor unboxing*

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.

Syntax Meets Semantics

Thursday December 7, 2023, 2PM, Salle 3052

**Pablo Barenbaum** (Universidad Buenos Aires) *Sharing in linear logic and call-by-need*

Syntax Meets Semantics

Thursday October 26, 2023, 2PM, salle 1007

**Giuseppe Castagna** (IRIF, CNRS and Univ. Paris Cite) *A type system for Elixir*

Syntax Meets Semantics

Thursday October 12, 2023, 2PM, salle 3052

**Mariana Milicich** (Université Paris Cité, CNRS, IRIF) *Useful Evaluation, Inductively and Quantitatively*

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.

Syntax Meets Semantics

Thursday September 28, 2023, 2PM, Salle 3052

**Beniamino Accattoli** (INRIA Saclay) *Closure Conversion and Abstract Machines*

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.

Syntax Meets Semantics

Thursday June 22, 2023, 2PM, salle 146 (Olympe de Gouges)

**Miguel Ramos** (Univ. Porto) *Quantitative CBV Global Memory*

Syntax Meets Semantics

Thursday June 1, 2023, 2PM, salle 146 (Olympe de Gouges)

**Gabriele Vanoni** (Univ. Bologna) *Higher-Order and Non-Linear Bayesian Networks*

Syntax Meets Semantics

Wednesday May 24, 2023, 2PM, salle 147 (Olympe de Gouges)

**Jose Espirito Santo** (Univ. Minho (Portugal)) *The logical essence of compiling with continuations*

Syntax Meets Semantics

Thursday April 20, 2023, 1:30PM, salle 147 (Olympe de Gouges)

**Hugo Herbelin** (IRIF, INRIA, Univ. Paris Cite) *Under syntax and semantics, the logic*

Syntax Meets Semantics

Thursday March 30, 2023, 1:30PM, salle 4052

**Nino Salibra** (Universita' Ca'Foscari Venezia) *A completeness theorem for the infinitary lambda calculus*

Syntax Meets Semantics

Tuesday March 28, 2023, 1:30PM, salle 3052

**Fabio Massaioli (Scuola Normale Di Pisa)** (Scuola Normale di Pisa) *A non-trivial proof-semantics for classical sequent calculus (LK)*

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.

Syntax Meets Semantics

Thursday March 9, 2023, 2PM, salle 1007

**Daniele Pautasso** (Univ. Torino) *A quantitative version of simple types*

Syntax Meets Semantics

Thursday March 2, 2023, 2PM, salle 1007

**Riccardo Treglia** *Intersecting effects: two orthogonal approaches*

Syntax Meets Semantics

Thursday February 9, 2023, 2PM, salle 1007

**Giovanni Bernardi** *Breaking circles*

Syntax Meets Semantics

Thursday January 26, 2023, 2PM, salle 1007

**Sandra Alves** *Quantitative Weak Linearisation*

Syntax Meets Semantics

Thursday January 12, 2023, 2PM, salle 1007

**Les Doctorants Du Groupe De Travail** (Universite Paris Cite) *Présentation des doctorants du groupe et de leur thématique de recherche*

#### Year 2022

Syntax Meets Semantics

Thursday December 15, 2022, 2PM, salle 1007

**Victor Arrial** *Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework*

Syntax Meets Semantics

Thursday November 3, 2022, 2PM, salle 1007

**Loic Peyrot** *Repetition soutenance de these*

Syntax Meets Semantics

Friday October 28, 2022, 2PM, salle 1007

**Pablo Barenbaum** *Proof Terms for Higher-Order Rewriting and Their Equivalence*

Syntax Meets Semantics

Wednesday October 19, 2022, 2PM, salle 1007

**Adrienne Lancelot** *Open Call-by-Value and Open Similarity*