## 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 22, 2023, 2PM, salle 146 (Olympe de Gouges)

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

Syntax Meets Semantics

Thursday September 7, 2023, 2PM, salle 146 (OdG)

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

### Previous talks

#### Year 2023

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*