License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.3
URN: urn:nbn:de:0030-drops-162840
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16284/
Go to the corresponding LIPIcs Volume Portal

Dagnino, Francesco ; Gavazzo, Francesco

A Fibrational Tale of Operational Logical Relations

pdf-format:
LIPIcs-FSCD-2022-3.pdf (0.9 MB)

Abstract

Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a λ-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations - a recently introduced notion of higher-order distance between programs - both pure and effectful, bringing them back to a common picture with traditional ones.

BibTeX - Entry

@InProceedings{dagnino_et_al:LIPIcs.FSCD.2022.3,
  author =	{Dagnino, Francesco and Gavazzo, Francesco},
  title =	{{A Fibrational Tale of Operational Logical Relations}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16284},
  URN =		{urn:nbn:de:0030-drops-162840},
  doi =		{10.4230/LIPIcs.FSCD.2022.3},
  annote =	{Keywords: logical relations, operational semantics, fibrations, generic effects, program distance}
}

Keywords: logical relations, operational semantics, fibrations, generic effects, program distance
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022

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