next day
all days

View: session overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
10:30-11:00Coffee Break
12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:30-15:30 Session 15B
Location: Ullmann 302
Recursive Session Logical Relations

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.

15:30-16:00Coffee Break
16:00-17:30 Session 19K
Location: Ullmann 302
Copromotion and Taylor Approximation (Work in Progress)
PRESENTER: Jean-Simon Lemay

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.

Denotational semantics driven simplicial homology?

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.

Bottom-Up Sequentialization of Unit-Free MALL Proof Nets
PRESENTER: Rémi Di Guardia

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.