ABSTRACT. We exhibit a formula in the language of system F which is provable in classical linear logic (when implication is interpreted as a linear one) but not in system F.

ABSTRACT. Proofs in a logic are usually considered (at least) up to cut-elimination. This is the case in linear logic, that also has another equivalence relation on proofs: rule commutation. We prove that these two notions coincide in second-order linear logic and many of its fragments. Moreover, we show that equality up to rule commutation is undecidable in propositional linear logic—and so is equality up to cut-elimination.

ABSTRACT. We investigate a property that extends the Danos-Regnier correctness criterion for linear logic proof-structures. The property applies to the correctness graphs of a proof-structure: it states that any such graph is acyclic and the number of its connected components is exactly one more than the number of nodes bottom or weakening. This is known to be necessary but not sufficient in multiplicative exponential linear logic to recover a sequent calculus proof from a proof-structure. We present a geometric condition allowing us to turn this necessary property into a sufficient one: we can thus isolate fragments of linear logic for which this property is indeed a correctness criterion. In intuitionistic linear logic, the property is equivalent to the familiar requirement of having exactly one output conclusion, and is sufficient for sequentialization in the fragment corresponding to the half-polarized typing system for call-by-push-value by Ehrhard.

ABSTRACT. Tensorial logic is a primitive logic of sum, tensor and negation which refines linear logic by relaxing the requirement that linear negation is involutive. The logic is designed in such a way that its formulas [modulo canonical isomorphism] are in a one-to-one correspondence with dialogue games, and that its proofs [modulo cut-elimination] are in a one-to-one correspondence with innocent strategies. In this paper, we explain how to accommodate the exponential modality of linear logic $A\mapsto {!\,A}$ and extend our functorial and proof-theoretic approach to game semantics beyond the multiplicative and additive fragment of tensorial logic. The extension relies on a notion of relative linear-non-linear adjunction on a dialogue category which refines the traditional notion of linear-non-linear adjunction on a $\ast$-autonomous category. In this description of full propositional tensorial logic, every exponential modality of linear logic $A\mapsto {!\,A}$ is attached to a negation of tensorial logic $A\mapsto \tensorialnegation{A}$. Two forms of negations thus coexist in the logic: the original non-involutive tensorial negation $A\mapsto \tensorialnegation{A}$ and a new backtracking exponential negation $A\mapsto\, \pointednegation{A}$ which stands for the ``modality + negation'' combinator~$A\mapsto \, !\, \lnot\, A$ and defines a relative comonad on the linear non-involutive negation.

ABSTRACT. Differential privacy is considered to be the golden standard in private data analysis. However, verifying that programs satisfy this standard is notoriously hard. The purpose of this submission is to report on an ongoing work of translating the Fuzz type system into a higher order logic RHOL. Fuzz is a type system used to prove sensitivity of programs, which is a very important property in differential privacy. Type systems, like Fuzz, are very convenient, because they allow for automation of proofs. Their downside is that they are less expressive than logics. With our work, we would like to combine the advantage of automated reasoning using Fuzz with the expressivity of RHOL. We provide the translation of the deterministic part of Fuzz, while our future goal is to extend it to the probabilistic part.

ABSTRACT. The connection between linear logic and process calculi has been studied for decades and is now well-established. In ongoing work, we have developed a new type system for the asynchronous pi-calculus based on linear logic, which enforces deadlock and lock freedom without imposing any determinism, termination or acyclic conditions coming from proofs. We introduce fixpoint replication, a new process construct that expresses recursion with simple types, like the fixpoint combinator in PCF. Fixpoint replication is justified by a natural generalization of the promotion rule in linear logic. Our work provides a unifying view on approaches to concurrency based on session types and on differential linear logic, in which logical features (cocontraction, fixpoints, logical correctness) correspond to behavioral features (non-determinism, non-termination, acyclicity) and may be modularly combined.

ABSTRACT. Linear logic admits a wide range of semantic presentations. One well-known example is phase semantics: an algebraic semantics in which formulas are interpreted in phase spaces, consisting of a commutative monoid and a fixed subset, with respect to which an orthogonality relation is defined. A rather different and much more recent approach is given by base-extension semantics, which defines validity by inductively extending a provability relation on a base -- a set of inference rules over atomic propositions. We establish an equivalence between the two semantics by first defining bidirectional maps between bases and phase spaces, and then constructing an isomorphism between a phase space (resp. base) and its image under the composition of these maps.

ABSTRACT. It is folklore that there is a tight link between biorthogonal-closure constructions, familiar to practitioners of linear logic, and logical relations, as they appear in, for instance reducibility-candidate flavoured proofs of normalisation for typed lambda calculi. One manifestation of this is in the technique of adapted pairs, due to Krivine [17], which weakens the extensionality condition defining a logical relation to facilitate the required induction over types [18]. In this technique, the full logical-relation condition appears as a kind of fixed-point of the adapted-pair condition. We aim to reformulate the duality underlying the definition of adapted pairs using linear logic, and connect this duality to techniques for proving denotational completeness (or definability) in models of the same [20].