Interaction Improvement

Adrienne Lancelot; Giulio Manzonetto; Guy McCusker; Gabriele  Vanoni

Interaction Improvement

Adrienne Lancelot, Giulio Manzonetto, Guy McCusker, Gabriele Vanoni

Research output: Contribution to conference › Paper › peer-review

Abstract

The relational semantics of linear logic is a powerful framework for defining resource-aware models of the lambda-calculus.
However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on lambda-terms, and demonstrate that it coincides with the preorder associated to the relational semantics.

Original language	English
Number of pages	44
Publication status	Acceptance date - 29 Apr 2026

Access to Document

https://arxiv.org/abs/2601.01638Licence: CC BY-SA

Cite this

@conference{2e357924756e42859f8c11a61c3e0a26,

title = "Interaction Improvement",

abstract = "The relational semantics of linear logic is a powerful framework for defining resource-aware models of the lambda-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between B{\"o}hm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on lambda-terms, and demonstrate that it coincides with the preorder associated to the relational semantics. ",

author = "Adrienne Lancelot and Giulio Manzonetto and Guy McCusker and Gabriele Vanoni",

year = "2026",

month = apr,

day = "29",

language = "English",

}

TY - CONF

T1 - Interaction Improvement

AU - Lancelot, Adrienne

AU - Manzonetto, Giulio

AU - McCusker, Guy

AU - Vanoni, Gabriele

PY - 2026/4/29

Y1 - 2026/4/29

N2 - The relational semantics of linear logic is a powerful framework for defining resource-aware models of the lambda-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on lambda-terms, and demonstrate that it coincides with the preorder associated to the relational semantics.

AB - The relational semantics of linear logic is a powerful framework for defining resource-aware models of the lambda-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on lambda-terms, and demonstrate that it coincides with the preorder associated to the relational semantics.

M3 - Paper

ER -

Interaction Improvement

Abstract

Access to Document

Fingerprint

Cite this