Published: 16th February 2015
DOI: 10.4204/EPTCS.176
ISSN: 2075-2180

EPTCS 176

Proceedings Third International Workshop on
Linearity
Vienna, Austria, 13th July, 2014

Edited by: Sandra Alves and Iliano Cervesato

Preface
Sandra Alves and Iliano Cervesato
Undecidability of Multiplicative Subexponential Logic
Kaustuv Chaudhuri
1
A Linear/Producer/Consumer Model of Classical Linear Logic
Jennifer Paykin and Steve Zdancewic
9
Cut Elimination in Multifocused Linear Logic
Taus Brock-Nannestad and Nicolas Guenot
24
Type Classes for Lightweight Substructural Types
Edward Gan, Jesse A. Tov and Greg Morrisett
34
Ludics without Designs I: Triads
Michele Basaldella
49
Wave-Style Token Machines and Quantum Lambda Calculi
Ugo Dal Lago and Margherita Zorzi
64
Geometry of Resource Interaction – A Minimalist Approach
Marco Solieri
79

Preface

This volume contains the post-proceedings of LINEARITY 2014, the Third International Workshop on Linearity, held on July 13, 2014 in Vienna, Austria. The workshop was a one-day satellite event of FLoC 2014, the sixth Federated Logic Conference. It was held as part of the 2014 Vienna Summer of Logic.

The program committee selected ten papers for presentation at LINEARITY 2014. In addition, the program included invited talks by Ian Mackie (École Polytechnique, France) and Elaine Pimentel (UFRN, Brazil). After the workshop, the authors were invited to submit a final, revised version of their paper for consideration for the post-proceedings to be published in EPTCS. The program committee selected seven papers, which are presented in this volume.

Ever since Jean-Yves Girard unveiled linear logic, linearity has played an important role in research spanning both theoretical investigations and applications to many areas of Computer Science. In the last 25 year, linearity has influenced our views on proof technology, complexity classes, quantum computation, program analysis, expressive operational semantics, linear programming languages, and techniques for program transformation, update analysis, and efficient implementation, just to cite a few.

The aim of this workshop was to bring together researchers who are exploring theory and applications of linear calculi, to foster their interaction and provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. Of interest were new results that made a central use of linearity, ranging from foundational work to applications in any field. This included: 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. Previous editions of LINEARITY were held in 2012 (Tallinn, Estonia) and 2009 (Coimbra, Portugal).

Many people helped make LINEARITY 2014 a success. We wish to thank the organizers of FLoC 2014 and of the Vienna Summer of Logic for their support. We are indebted to the program committee members and the external referees for their careful and efficient work in the reviewing process. Finally we are grateful to the authors, the invited speakers and the attendees who made this workshop an enjoyable and fruitful event.

Sandra Alves and Iliano Cervesato
January, 2015

Program Committee of LINEARITY 2014

Additional Reviewers

Taus Brock-Nannestad, Sabine Broda, Alessandra Di Pierro, Chris Martens, Dimitris Mostrous, Michele Pagani, Nicolas Pouillard, Benoît Valiron, and Pedro Vasconcelos.