Repository logo
 

Fixpoint constructions in focused orthogonality models of linear logic

Published version
Peer-reviewed

Repository DOI


Type

Conference Object

Change log

Authors

Galal, Zeinab 
Jafarrahmani, Farzad 

Abstract

jats:pOrthogonality 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.</jats:p>

Description

Keywords

5003 Philosophy, 4904 Pure Mathematics, 49 Mathematical Sciences, 50 Philosophy and Religious Studies

Journal Title

Electronic Notes in Theoretical Informatics and Computer Science

Conference Name

MFPS 2023

Journal ISSN

2969-2431
2969-2431

Volume Title

Volume 3 - Proceedings of...

Publisher

Centre pour la Communication Scientifique Directe (CCSD)
Sponsorship
EPSRC (EP/V002309/1)
EPSRC grant EP/V002309/1