Contraposition is the classical reasoning principle stating that A → B is equivalent to ¬B → ¬A. In typical presentations of classical Linear Logic, e.g. those based on sequent calculus or proof nets, contraposition has no significant computational content, as it corresponds basically to a change of notation. However, for systems in natural deduction style, contraposition exchanges the role of an assumption and a conclusion, which requires to perform a global transformation on the proof. We propose a term calculus for MELL in which contraposition is realized by an operator we dub contrasubstitution, which turns a proof “inside out” to exchange the roles of the conclusion and a specific assumption. We study the properties of this calculus, starting by confluence and strong-normalization. We identify an intuitionistic fragment and show that it simulates various existing classical calculi (such as Parigot's lambda-mu) via Danos et al.'s Q and T translations.

Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.

In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as B, the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.

Session types are a typed approach to ensure the communication correctness of message-passing programs. They have been extensively studied from a theoretical standpoint, and have been also incorporated into diverse programming languages and models.

Perhaps surprisingly, there is no single, canonical session type system, but many. It is fair to say that expressiveness has been key to the success and impact of session types: enhancing the expressivity of typed processes and/or the properties enforced by typing is often a strong motivation for developing new typed frameworks.

In this rich and diverse context, rigorously contrasting different variants of session types from an expressiveness perspective is a fascinating and non-trivial challenge. In this talk I introduce session types briefly and overview some recent works related to their expressiveness; they cover various angles, including “propositions-as-sessions”, i.e., the Curry-Howard correspondence between session types and linear logic.

In this talk, we will discuss the strength of embedding Call-by-Name (dCBN) and Call-by-Value (dCBV) into a unifying framework called the Bang Calculus (dBANG). These embeddings enable establishing (static and dynamic) properties of dCBN and dCBV through their respective counterparts in dBANG. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) dCBN case, while a novel one must be introduced for the (difficult) dCBV case. Moreover, a key point of our approach is the identification of dBANG diligent reduction sequences, which eases the preservation of dynamic properties from dBANG to dCBN/dCBV. We illustrate our methodology through two concrete applications: confluence/factorization for both dCBN and dCBV are respectively derived from confluence/factorization for dBANG.

Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value.

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.

I will present a type system based on non-idempotent intersection types for PCFh, a variant of PCF. Evaluation in PCFh is hybrid: call-by-name (CBN) and call-by-value (CBV) behaviours cohabit together. Specifically, function application follows CBV semantics, while recursion has a CBN flavour. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFh evaluation. This means not only that typability implies normalisation, but also that the converse holds. Moreover, the type system is quantitative, since the size of typing derivations provides upper bounds for the length of normalisation sequences. By refining this type system, we obtain a tight type system, which offers exact information regarding the length of normalisation sequences.

I will give an introduction to type refinement systems in the style of Frank Pfenning et al., discuss the phenomenon of how refinement typing makes some aspects of evaluation order visible in the type system, and give some general indications of how type refinement may be understood from a categorical perspective. For background reading, you can see my notes from OPLSS 2016 on “Principles of type refinement” (https://noamz.org/oplss16/refinements-notes.pdf).

Dans le but de factoriser et étendre les techniques d'Analyses Amorties de Ressource Automatisées, nous introduisons une machine abstraite comme représentation intermédiaire pour étendre les possibilités d'analyses aux langages linéaires et à sémantiques Call-By-Push-Value (CBPV), qui intègre à la fois l'appel par valeur et l'appel par nom.

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

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

Structural proof theory has been widely used in the study of term structures. In this talk, I will illustrate this tight connection between proofs and terms by presenting the focused proof system LJF as a framework for designing term structures. Since the proof theory of LJF does not pick a canonical polarization for atomic formulas, two different approaches to term representation arise. We will illustrate these two approaches by applying them to the encoding of untyped lambda terms. When atomic formulas are given the negative polarity, LJF proofs yield the usual tree-like representation of untyped lambda terms. When atomic formulas are given the positive polarity, LJF proofs yield a term structure in which sharing is possible via explicit substitution. In the second part of the talk, I will present the positive lambda calculus, a calculus with explicit substitution based on the positive polarization, and show its close relationship with Accattoli and Paolini's value substitution calculus.