Published: 17th January 2017
DOI: 10.4204/EPTCS.238
ISSN: 2075-2180


Proceedings Fourth International Workshop on
Porto, Portugal, 25 June 2016

Edited by: Iliano Cervesato and Maribel Fernández

A Proof Theory for Model Checking: An Extended Abstract
Quentin Heath and Dale Miller
Proof Diagrams for Multiplicative Linear Logic
Matteo Acclavio
Krivine Machine and Taylor Expansion in a Non-uniform Setting
Antoine Allioux
Surface Proofs for Nonsymmetric Linear Logic (Extended Abstract)
Lawrence Dunn and Jamie Vicary
Linear β-reduction
Stefano Guerrini
Linear Exponential Comonads without Symmetry
Masahito Hasegawa
Non-Blocking Concurrent Imperative Programming with Session Types
Miguel Silva, Mário Florido and Frank Pfenning
Design and Implementation of Concurrent C0
Max Willsey, Rokhini Prabhu and Frank Pfenning


Since the birth of linear logic, there has been a stream of research where linearity is a key issue, covering both theoretical topics and applications to several areas of Computer Science, such as work on proof technology, complexity classes and more recently quantum computation, program analysis, expressive operational semantics, linear programming languages, and techniques for program transformation, update analysis and efficient implementation.

The LINEARITY workshops bring together researchers who are developing theory and applications of linear calculi. The main goals are to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. Topics of interest include: sub-linear logics, linear term calculi, linear type systems, linear proof theory, linear programming languages, applications to concurrency, interaction-based systems, verification of linear systems, quantum models of computation, and biological and chemical models of computation.

This volume contains the post-proceedings of LINEARITY 2016, the Fourth International Workshop on Linearity, held on June 25, 2016 in Porto, Portugal. The workshop was affiliated with FSCD 2016, the International Conference on Formal Structures for Computation and Deduction.

The programme committee selected seven papers for presentation at LINEARITY 2016. In addition, the programme included invited talks by Dale Miller (Ecole Polytechnique, France) and by Daniyar Shamkanov (National Research University, Russia). This volume contains revised versions of the papers presented at the workshop.

Previous editions of LINEARITY were held in 2014 (Vienna, Austria), 2012 (Tallinn, Estonia) and 2009 (Coimbra, Portugal).

We would like to thank all those who contributed to LINEARITY 2016, in particular the authors of the submitted papers, the invited speakers who kindly accepted to present their work at LINEARITY, the participants and the local organisers of the FSCD conference. Easychair was used to manage submissions and to generate the pre-proceedings. Special thanks to the Programme Committee members and external reviewers for their support and efficient work, and to EPTCS for the publication of the final proceedings.

Iliano Cervesato and Maribel Fernández
November 2016

Programme Committee of LINEARITY 2016

Additional Reviewers

Stefano Guerrini (Université Paris 13), Alexandre Miquel (Universidad de la República), Philip Scott (University of Ottawa).

Local Organisers

Sandra Alves and Sabine Broda (University of Porto).