Francesco Dagnino ; Francesco Gavazzo - A Fibrational Tale of Operational Logical Relations: Pure, Effectful and Differential

lmcs:11041 - Logical Methods in Computer Science, April 4, 2024, Volume 20, Issue 2 -
A Fibrational Tale of Operational Logical Relations: Pure, Effectful and DifferentialArticle

Authors: Francesco Dagnino ; Francesco Gavazzo

    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 lambda-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.

    Volume: Volume 20, Issue 2
    Published on: April 4, 2024
    Accepted on: February 29, 2024
    Submitted on: March 7, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 644 times.
    This article's PDF has been downloaded 376 times.