Delia Kesner

CSL Conference 2026 Conference Paper

Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

• Pablo Barenbaum
• Delia Kesner
• Mariana Milicich

Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.

LPAR Conference 2024 Conference Paper

Hybrid Intersection Types for PCF

• Pablo Barenbaum
• Delia Kesner
• Mariana Milicich

Intersection type systems have been independently applied to different evaluation strate- gies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together, without making use of an encoding into a common target framework. This work proposes an intersection type system for a specific notion of evaluation for PCF, called PCFH. Evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV- like behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the reduction sequences to normal form. This first type system is then refined to a tight one, offering exact information regarding the length of normalization sequences. This is the first time that a sound and complete quantitative type system has been designed for a hybrid computational model.

FSCD Conference 2024 Conference Paper

Meaningfulness and Genericity in a Subsuming Framework (Invited Talk)

• Delia Kesner
• Victor Arrial
• Giulio Guerrieri

This paper studies the notion of meaningfulness for a unifying framework called dBang-calculus, which subsumes both call-by-name (dCBN) and call-by-value (dCBV). We first define meaningfulness in dBang and then characterize it by means of typability and inhabitation in an associated non-idempotent intersection type system previously appearing in the literature. We validate the proposed notion of meaningfulness by showing two properties: (1) consistency of the smallest theory, called ℋ, equating all meaningless terms, and (2) genericity, stating that meaningless subterms have no bearing on the significance of meaningful terms. The theory ℋ is also shown to have a unique consistent and maximal extension ℋ*, which coincides with a well-known notion of observational equivalence. Last but not least, we show that the notions of meaningfulness and genericity in the literature for dCBN and dCBV are subsumed by the corresponding ones proposed here for the dBang-calculus.

CSL Conference 2024 Conference Paper

The Ackermann Award 2023

• Maribel Fernández
• Jean Goubault-Larrecq
• Delia Kesner

Report on the 2023 Ackermann Award.

I&C Journal 2023 Journal Article

The bang calculus revisited

• Antonio Bucciarelli
• Delia Kesner
• Alejandro Ríos
• Andrés Viso

Call-by-Push-Value (CBPV) is a programming paradigm subsuming both Call-by-Name (CBN) and Call-by-Value (CBV) semantics. The essence of this paradigm is captured by the Bang Calculus, a term language connecting CBPV and Linear Logic. This paper presents a revisited version of the Bang Calculus, called λ! , enjoying some important properties missing in the original formulation. Indeed, the new calculus integrates permutative conversions to unblock value redexes while preserving confluence. A second contribution is related to non-idempotent types. We provide a quantitative type system for our λ! -calculus, giving upper bounds to the length of the reduction to normal form plus its size. We also explore the properties of this type system with respect to CBN/CBV translations. Last but not least, the quantitative system is refined to a tight one, which transforms the previous upper bound into two independent exact measures for the reduction length and the normal form size respectively.

CSL Conference 2022 Conference Paper

Encoding Tight Typing in a Unified Framework

• Delia Kesner
• Andrés Viso

This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, i. e. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.

FSCD Conference 2022 Conference Paper

Solvability for Generalized Applications

• Delia Kesner
• Loïc Peyrot

Solvability is a key notion in the theory of call-by-name lambda-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation - such as call-by-value -, is not straightforward. In this paper, we study solvability for call-by-name and call-by-value lambda-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the lambda-calculus are equivalent notions.

CSL Conference 2020 Conference Paper

Strong Bisimulation for Control Operators (Invited Talk)

• Delia Kesner
• Eduardo Bonelli
• Andrés Viso

The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation ≃, defined over a revised presentation of Parigot’s λμ-calculus we dub ΛM. Our result builds on two fundamental ingredients: (1) factorization of λμ-reduction into multiplicative and exponential steps by means of explicit term operators of ΛM, and (2) translation of ΛM-terms into Laurent’s polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation ≃ is shown to characterize structural equivalence in PPN. Most notably, ≃ is shown to be a strong bisimulation with respect to reduction in ΛM, i. e. two ≃-equivalent terms have the exact same reduction semantics, a result which fails for Regnier’s σ-equivalence in λ-calculus as well as for Laurent’s σ-equivalence in λμ.

TCS Journal 2017 Journal Article

On abstract normalisation beyond neededness

• Eduardo Bonelli
• Delia Kesner
• Carlos Lombardi
• Alejandro Ríos

We study normalisation of multistep strategies, strategies that reduce a set of redexes at a time, focusing on the notion of necessary sets, those which contain at least one redex that cannot be avoided in order to reach a normal form. This is particularly appealing in the setting of non-sequential rewrite systems, in which terms that are not in normal form may not have any needed redex. We first prove a normalisation theorem for abstract rewrite systems (ARS), a general rewriting framework encompassing many rewriting systems developed by P-A. Melliès [20]. The theorem states that multistep strategies reducing so called necessary and never-gripping sets of redexes at a time are normalising in any ARS. Gripping refers to an abstract property reflecting the behaviour of higher-order substitution. We then apply this result to the particular case of PPC, a calculus of patterns and to the lambda-calculus with parallel-or.

TCS Journal 2015 Journal Article

Special Issue: Selected papers of the 7th and 8th workshops on Logical and Semantic Frameworks with Applications (LSFA)

• Marcelo Finger
• Delia Kesner

LPAR Conference 2012 Conference Paper

The Permutative λ-Calculus

• Beniamino Accattoli
• Delia Kesner

Abstract We introduce the permutative λ -calculus, an extension of λ -calculus with three equations and one reduction rule for permuting constructors, generalising many calculi in the literature, in particular Regnier’s sigma-equivalence and Moggi’s assoc-equivalence. We prove confluence modulo the equations and preservation of beta-strong normalisation (PSN) by means of an auxiliary substitution calculus. The proof of confluence relies on M-developments, a new notion of development for λ -terms.

TCS Journal 2011 Journal Article

A prismoid framework for languages with resources

• Delia Kesner
• Fabien Renaud

Inspired by the Multiplicative Exponential fragment of Linear Logic, we define a framework called the prismoid of resources where each vertex is a language which refines the λ -calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β -reduction, confluence, preservation of β -strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter of the formalism, so that all the properties for each vertex are obtained as a particular case of the general abstract proofs.

CSL Conference 2010 Conference Paper

The Structural lambda -Calculus

• Beniamino Accattoli
• Delia Kesner

Abstract Inspired by a recent graphical formalism for λ -calculus based on Linear Logic technology, we introduce an untyped structural λ -calculus, called λj, which combines action at a distance with exponential rules decomposing the substitution by means of weakening, contraction and dereliction. Firstly, we prove fundamental properties such as confluence and preservation of β -strong normalisation. Secondly, we use λj to describe known notions of developments and superdevelopments, and introduce a more general one called XL -development. Then we show how to reformulate Regnier’s σ -equivalence in λj so that it becomes a strong bisimulation. Finally, we prove that explicit composition or de-composition of substitutions can be added to λj while still preserving β -strong normalisation.

MFCS Conference 2009 Conference Paper

The Prismoid of Resources

• Delia Kesner
• Fabien Renaud

Abstract We define a framework called the prismoid of resources where each vertex refines the λ -calculus by using a different choice to make explicit or implicit (meta-level) the definition of the contraction, weakening, and substitution operations. For all the calculi in the prismoid we show simulation of β -reduction, confluence, preservation of β -strong normalisation and strong normalisation for typed terms. Full composition also holds for all the calculi of the prismoid handling explicit substitutions. The whole development of the prismoid is done by making the set of resources a parameter, so that the properties for each vertex are obtained as a particular case of the general abstract proofs.

I&C Journal 2007 Journal Article

Resource operators for λ-calculus

• Delia Kesner
• Stéphane Lengrand

We present a simple term calculus with an explicit control of erasure and duplication of substitutions, enjoying a sound and complete correspondence with the intuitionistic fragment of Linear Logic’s proof-nets. We show the operational behaviour of the calculus and some of its fundamental properties such as confluence, preservation of strong normalisation, strong normalisation of simply typed terms, step by step simulation of β-reduction and full composition.

CSL Conference 2007 Conference Paper

The Theory of Calculi with Explicit Substitutions Revisited

• Delia Kesner

Abstract Calculi with explicit substitutions (ES) are widely used in different areas of computer science. Complex systems with ES were developed these last 15 years to capture the good computational behaviour of the original systems (with meta-level substitutions) they were implementing. In this paper we first survey previous work in the domain by pointing out the motivations and challenges that guided the development of such calculi. Then we use very simple technology to establish a general theory of explicit substitutions for the lambda-calculus which enjoys fundamental properties such as simulation of one-step beta-reduction, confluence on metaterms, preservation of beta-strong normalisation, strong normalisation of typed terms and full composition. The calculus also admits a natural translation into Linear Logic’s proof-nets.

TCS Journal 2004 Journal Article

Pattern matching as cut elimination

• Serenella Cerrito
• Delia Kesner

We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely Gentzen sequent calculus for intuitionistic minimal logic. Our calculus is inspired by the Curry–Howard Isomorphism, in the sense that types, both for patterns and terms, correspond to propositions, terms correspond to proofs, and term reduction corresponds to sequences of sequent proof normalization steps performed by cut elimination. The calculus enjoys subject reduction, confluence, preservation of strong normalization w. r. t a system with meta-level substitutions and strong normalization for well-typed terms. As a consequence, it can be seen as an implementation calculus for functional formalisms defined with meta-level operations for pattern matching and substitutions. This work is a revised and extended version of Cerrito and Kesner (14th Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1999, pp. 98–108).

TCS Journal 2000 Journal Article

Confluence of extensional and non-extensional λ-calculi with explicit substitutions

• Delia Kesner

This paper studies confluence of extensional and non-extensional λ-calculi with explicit substitutions, where extensionality is interpreted by η-expansion. For that, we propose a scheme for explicit substitutions which describes those abstract properties that are sufficient to guarantee confluence. Our method makes it possible to treat at the same time many well-known calculi such as λσ, λσ⇑, λφ, λs, λv, λf, λd and λdn.

MFCS Conference 1998 Conference Paper

Reducing AC-Termination to Termination

• Maria C. F. Ferreira
• Delia Kesner
• Laurence Puel

Abstract We present a new technique for proving AC-termination. We show that if certain conditions are met, AC-termination can be reduced to termination, i. e. , termination of a TRS S modulo an AC-theory can be inferred from termination of another TRS R with no AC-theory involved. This is a new perspective and opens new possibilities to deal with AC-termination.

I&C Journal 1996 Journal Article

A Typed Pattern Calculus

• Delia Kesner
• Laurence Puel
• Val Tannen

The theory of programming with pattern-matching function definitions has been studied mainly in the framework of first-order rewrite systems. We present a typed functional calculus that emphasizes the strong connection between the structures of whole pattern definitions and their types. In this calculus, type-checking guarantees the absence of runtime errors caused by non-exhaustive pattern-matching definitions. Its operational semantics is deterministic in a natural way, without the imposition of ad hoc solutions such as clause order or “best fit”. In the spirit of the Curry–Howard isomorphism, we design the calculus as a computational interpretation of the Gentzen sequent proofs for the intuitionistic propositional logic. We prove the basic properties connecting typing and evaluation: subject reduction and strong normalization. We believe that this calculus offers a rational reconstruction of the pattern-matching features found in successful functional languages.

TCS Journal 1996 Journal Article

Combining algebraic rewriting, extensional lambda calculi, and fixpoints

• Roberto Di Cosmo
• Delia Kesner

It is well known that confluence and strong normalization are preserved when combining algebraic rewriting systems with the simply typed lambda calculus. It is equally well known that confluence fails when adding either the usual contraction rule for η, or recursion together with the usual contraction rule for surjective pairing. We show that confluence and strong normalization are modular properties for the combination of algebraic rewriting systems with typed lambda calculi enriched with expansive extensional rules for η and surjective pairing. We also show how to preserve confluence in a modular way when adding fixpoints to different rewriting systems. This result is also obtained by a simple translation technique allowing to simulate bounded recursion.

CSL Conference 1996 Conference Paper

Rewriting with Extensional Polymorphic Lambda-Calculus

• Roberto Di Cosmo
• Delia Kesner

Abstract We provide a confluent and strongly normalizing rewriting system, based on expansion rules, for the extensional second order typed lambda calculus with product and unit types: this system corresponds to the Intuitionistic Positive Calculus with implication, conjunction, quantification over proposition and the constant True. This result is an important step towards a new theory of reduction based on expansion rules, and gives a natural interpretation to the notion of second order η-long normal forms used in higher order resolution and unification, that are here just the normal forms of our reduction system.

MFCS Conference 1991 Conference Paper

Pattern Matching in Order-Sorted Languages

• Delia Kesner

Abstract We study the problem of pattern matching in languages whose type system is hierarchical and whose evaluation strategy is lazy. We propose an extension of the Puel-Suárez compilation scheme to function definitions via order-sorted patterns. Pattern matching trees (PMT's) are defined to have edges labelled not only with structure, but also with subsort constraints. Due to this latter kind of edges, terms are reduced only as far as required to make either a structure or a subsort verification decidable. We show that the PMT is optimal if a decidable property of sequentiality holds for the sets generated during the compilation process. Our method turns out to be applicable for strict languages as well.