The relational model is injective for Multiplicative Exponential Linear Logic

The relational model is injective for Multiplicative Exponential Linear Logic (without weakenings)

We show that for Multiplicative Exponential Linear Logic (without weakenings) the syntactical equivalence relation on proofs induced by cut-elimination coincides with the semantic equivalence relation on proofs induced by the multiset based relational model: one says that the interpretation in the model (or the semantics) is injective. We actually prove a stronger result: two cut-free proofs of the full multiplicative and exponential fragment of linear logic whose interpretations coincide in the multiset based relational model are the same "up to the connections between the doors of exponentia…

Relational type-checking for MELL proof-structures. Part 1: Multiplicatives

Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $Γ$ acts thus as a type (refining $Γ$) having R as an inhabitant. We are interested in the following type-checking question: given a proof-structure R, a list of formulae $Γ$, and a point x in the relational interpretation of $Γ$, is x in the interpretation of R? This question is decidable. We present here an algorithm that decides it …

线性逻辑中的泰勒展开是可逆的

Taylor expansion in linear logic is invertible

本文证明MELL证明网的泰勒展开是单射的，即不同证明网对应不同展开，进而推出关系模型对MELL证明网的完备性，即相等性恰由消割公理化。

基于索引线性逻辑的MALL交互几何

A MALL Geometry of Interaction Based on Indexed Linear Logic

本文为乘法-加法线性逻辑构建基于索引线性逻辑的交互几何，扩展了Haghverdi-Scott范畴框架，利用索引处理加法消割的叠加、擦除和收缩，并证明执行公式沿消割不变，收敛到无割证明的指称。

在笛卡尔闭范畴上的全可定义性

Full Definability in a Profunctorial Model

本文研究了基于群oid上仿射范畴的模型中的全可定义性，证明了稳定且全的仿射在多价线性逻辑中可通过证明网络定义。

分支逻辑：通过有序分离

Bifurcation Logic: Separation Through Ordering

分支逻辑通过有序分离结合模态算子和分离 conjunction，用于多代理访问控制，提供了一种可判定的逻辑框架。