An infinitary model of linear logic

TL;DR

This paper develops an advanced infinitary relational model of linear logic incorporating countable multisets, fixpoint operators, and parity-based priorities, linking lambda-calculus recursion with higher-order model-checking.

Contribution

It introduces a novel infinitary relational model with parity-based fixpoint operators, bridging linear logic semantics with recursion and model-checking.

Findings

Defined a new infinitary relational model of linear logic

Extended semantics with parity-based priorities for fixpoints

Connected lambda-calculus recursion to higher-order model-checking

Abstract

In this paper, we construct an infinitary variant of the relational model of linear logic, where the exponential modality is interpreted as the set of finite or countable multisets. We explain how to interpret in this model the fixpoint operator Y as a Conway operator alternatively defined in an inductive or a coinductive way. We then extend the relational semantics with a notion of color or priority in the sense of parity games. This extension enables us to define a new fixpoint operator Y combining both inductive and coinductive policies. We conclude the paper by sketching the connection between the resulting model of lambda-calculus with recursion and higher-order model-checking.