ABSTRACT. Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types — but exclusively for terminating languages. In this talk, I develop a logical relation for an intuitionistic linear logic session type language with general recursive types and instantiate it for proving progress-sensitive noninterference. Concurrency and non-termination pose several challenges, and I explain how the logical relation addresses them. A distinguishing feature of the development is the choice of an observational step index, which ensures compositionality and proofs of transitivity and soundness.

ABSTRACT. Quantitative models of Linear Logic, where non-linear proofs are interpreted by power series, hold a special place in the semantics of linear logic. They are at the heart of Differential Linear Logic and its application to probabilistic programming and new proofs methods in lambda-calculus. In this abstract, we explore a refinement of DiLL with a copromotion rule, modelized by categories where all maps are quantitative.

ABSTRACT. Linear logic’s coherent spaces are a simple kind of abstract simplicial complexes (asc, for short). These combinatorially encode a topological space that is usually studied via (simplicial) homology. We can easily associate an asc with any formula of LL under some semantics, in such a way proofs become the faces of the asc and such that this asc satisfactorily represents the “space of the (interpretations of the) proofs” of the formula. Starting from this remark, we discuss the natural question of defining a type-isomorphic invariant homology for those asc’s.

ABSTRACT. We propose a new proof of sequentialization for the proof nets of unit-free multiplicative-additive linear logic of Hughes & Van Glabbeek. This is done by adapting a method from unit-free multiplicative linear logic, showing the robustness of this approach.