Skip to Main content Skip to Navigation
Conference papers

Differential Logical Relations Part I: The Simply-Typed Case

Ugo Dal Lago 1, 2 Francesco Gavazzo 3, 2 Akira Yoshimizu 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category.
Document type :
Conference papers
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Francesco Gavazzo <>
Submitted on : Friday, November 29, 2019 - 10:51:53 AM
Last modification on : Friday, July 9, 2021 - 5:18:01 PM


Files produced by the author(s)




Ugo Dal Lago, Francesco Gavazzo, Akira Yoshimizu. Differential Logical Relations Part I: The Simply-Typed Case. ICALP 2019 - 46th International Colloquium on Automata, Languages and Programming, Jul 2019, Patras, Greece. ⟨10.4230/LIPIcs.ICALP.2019.XXX⟩. ⟨hal-02386110⟩