Substructural logics: semantics, proof theory, and applications

26–28 February 2018, Vienna (Austria)

Second SYSMICS Workshop

Giada Coppi

Invited Speakers

Matteo Maffei (Vienna)

Title: Security and Privacy by Typing in Cryptographic Systems

The security of modern distributed systems is an important and complex challenge, which has attracted the interest of a growing research community over the last decade. The cryptographic protocols used to securely transmit data over an untrusted network, and even more so their software implementations, are extraordinarily difficult to design and to prove secure, as witnessed by the continuously growing list of discovered vulnerabilities. The complexity of cryptographic systems stem from several factors and has significantly increased over the years. First of all, while early academic protocols mostly consisted of simple combinations of signature and encryption schemes, modern ones rely on much more sophisticated, and arguably fascinating, cryptographic primitives, such as zero-knowledge proofs and secure multiparty computations. Secondly, the security and privacy properties required by modern applications go well beyond the well-understood secrecy and authenticity properties, covering, e.g., indistinguishability relations and differential privacy.

Language-based techniques, and type systems in particular, lived up to the challenge, constituting a solid and expressive framework for the verification and design of cryptographic systems. While early academic cryptographic protocols required relatively simple type and effect systems, modern cryptography called for more powerful techniques, such as refinement types, union and intersection types, linear types, and relational refinements.

The goal of this talk is to guide the audience through the literature on type theory for cryptographic applications, giving a consolidated view of the research development in this field and establishing bridges with various subdisciplines of interest to the logic, semantics, and verification community (e.g., type theory, SMT solving, linear logic, proof-carrying authorization, relational verification, and concurrent programming), with the final goal of fostering cross-fertilizing research ideas.

Francesco Paoli (Cagliari)

Title: The Archimedean Property: New Horizons and Perspectives Joint work with Antonio Ledda and Constantine Tsinakis

Although there have been repeated attempts to define the concept of an Archimedean algebra for individual classes of residuated lattices, there is no all-purpose definition that suits the general case. We suggest as a possible candidate the notion of a normal-valued and $e$-cyclic residuated lattice that has the \emph{zero radical compact property} --- namely, a normal-valued and $e$-cyclic residuated lattice in which every principal convex subuniverse has a trivial radical (understood as the intersection of all its maximal convex subuniverses). We characterize the Archimedean members in the variety of $e$-cyclic residuated lattices, as well as in various special cases of interest. A theorem to the effect that each Archimedean and prelinear GBL-algebra is commutative, subsuming as corollaries several analogous results from the recent literature, is grist to the mill of our proposal's adequacy.

Elaine Pimentel (Natal)

Title: A unified view of modal and substructural logics

It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a cut-free, general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring different axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for different logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems.

This is a joint work with Björn Lellmann and Carlos Olarte.

David Pym (London)

Title: Logic as a modelling technology: resource semantics, systems modelling, and security

The development of BI, the logic of bunched implications, together with its resource semantics, led to the formulation of Separation Logic, which forms the basis of the Infer program analyser deployed in Facebook's code production. However, this rather successful story sits within a broader, quite systematic logical context. I will review the (family of) logics, including process logics, that are supported by resource semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating their uses in a range of modelling applications, including access control, systems security, and workflow simulation.

Alwen Tiu (Canberra)

Title: A proof theory for dual nominal quantifiers

One approach in relating logic and process calculus is via the formula-as-process interpretation, where process constructors are interpreted by logical connectives. In this talk I will discuss a problem of embedding the pi-calculus in linear logic, and highlight some problems with the interpretation of the restriction operator of the pi-calculus as a quantifier in logic. In particular, I will show that self-dual nominal quantifiers, such as Gabbay and Pitts's new quantifier or Miller and Tiu's nabla quantifier are both unsuitable in this setting. A key requirement seems to be that the nominal quantifier must not distribute over the par connective. This motivated a recent work on the introduction of a dual pair of nominal quantifiers, called `new' and `wen', where the distributivity property of par is absent. The proof rules for the `new' quantifier have a similar flavour to the universal quantifier rules, whereas the `wen' quantifier rules are similar to the existential ones, except that the wen-quantified variable can only be instantiated with a fresh name. I will present a proof system featuring these dual nominal quantifiers, extending the BV proof system for a non-commutative multiplicative linear logic. I will sketch the cut-elimination proof and show how one can interpret pi-processes in logic such that implication gives rise to a process pre-order. I will then discuss some open problems, in particular, in the interaction between the nominal quantifiers and the sequential operator of BV.

This talk is based on a joint work with Ross Horne, Bogdan Aman, and Gabriel Ciobanu.

Philip Wadler (Edinburgh)

Title: Propositions as Sessions

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions of classical linear logic correspond to session types. Continuing a line of work by Honda (1993), by Honda, Kubo, and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others, this paper presents GV, a linear functional language with session types, and presents a translation from GV into CP. The translation formalises for the first time a connection between a standard presentation of session types and linear logic, and shows how a modification to the standard presentation yield a language free from deadlock, where deadlock freedom follows from the correspondence to linear logic.