License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2019.111
URN: urn:nbn:de:0030-drops-106879
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10687/
Go to the corresponding LIPIcs Volume Portal

Dal Lago, Ugo ; Gavazzo, Francesco ; Yoshimizu, Akira

Differential Logical Relations, Part I: The Simply-Typed Case

pdf-format:
LIPIcs-ICALP-2019-111.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{dallago_et_al:LIPIcs:2019:10687,
  author =	{Ugo Dal Lago and Francesco Gavazzo and Akira Yoshimizu},
  title =	{{Differential Logical Relations, Part I: The Simply-Typed Case}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{111:1--111:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Christel Baier and Ioannis Chatzigiannakis and Paola Flocchini and Stefano Leonardi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10687},
  URN =		{urn:nbn:de:0030-drops-106879},
  doi =		{10.4230/LIPIcs.ICALP.2019.111},
  annote =	{Keywords: Logical Relations, lambda-Calculus, Program Equivalence, Semantics}
}

Keywords: Logical Relations, lambda-Calculus, Program Equivalence, Semantics
Collection: 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)
Issue Date: 2019
Date of publication: 04.07.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI