Marcelo Fiore ; Zeinab Galal ; Farzad Jafarrahmani - Fixpoint constructions in focused orthogonality models of linear logic

entics:12302 - Electronic Notes in Theoretical Informatics and Computer Science, November 23, 2023, Volume 3 - Proceedings of MFPS XXXIX - https://doi.org/10.46298/entics.12302
Fixpoint constructions in focused orthogonality models of linear logicArticle

Authors: Marcelo Fiore ; Zeinab Galal ; Farzad Jafarrahmani

    Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.


    Volume: Volume 3 - Proceedings of MFPS XXXIX
    Published on: November 23, 2023
    Accepted on: October 16, 2023
    Submitted on: September 20, 2023
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Category Theory

    Consultation statistics

    This page has been seen 132 times.
    This article's PDF has been downloaded 113 times.