**Organizers:** Ugo Dal Lago,
Marco Gaboardi,
Dan Ghica,
Damiano Mazza,
Guy McCusker,
Michele Pagani,
Ulrich Schoepp,
Christine Tasson

In the last couple of years we have seen several interesting and exciting new applications of bounded linear type systems to resource management and control. As a result, a group of us will organize a small workshop dedicated to the study of such type systems, their semantics and their applications. The workshop will be held at the Fontainbleau research center of Universite Paris 7 in the first week of December (2-4). This will be a true workshop, focusing primarily on developing new ideas and collaborations, rather than on talks. There will be no fee for the workshop itself. The invited participants are listed here.

The workshop hotel is the Ibis hotel in Fontainebleau. Arrival information can be accessed here.

Lunches will be provided, but you will need to pay for dinner. We plan to go out together to a restaurant in Fontainebleau. The expect cost of the dinner is about EUR20. Please let us know if you would like to go for dinner Monday and/or Tuesday to make reservations.

**Monday**- 9h-9h45: Steve Zdancewic: Linear logic and linear algebra [slides]
- 9h45-10h30: Paul-Andre Mellies: Sharing and duplication in tensorial logic
- break
- 11h-11h45: Jim Laird: Quantitative models of mobile processes
- 11h45-12h30: Ulrich Schoepp: CBN, CBV and a primitive logic for interaction
**Tuesday**- 9h-9h45: Dan R. Ghica: BLL over a semiring with applications [slides]
- 9h45-10h30: Damiano Mazza: Linear Approximations, Continuity and the Cook-Levin Theorem [slides]
- break
- 11h-11h45: Flavien Breuvart: A bridge between semirings [slides]
- 11h45-12h30: Marco Gaboardi: Combining bounded exponential and co-effects [slides]
**Wednesday**- 9h-9h45: Benoit Valiron: Automated resource estimation in quantum algorithms
- 9h45-10h30: Ugo Dal Lago: Linear dependent types in a subrecursive setting [slides]
- break
- 11h-11h45: Fredrik Nordvall Forsberg: Restricted linear dependent types [slides]
- 11h45-12h30: Neel Krishnaswami: Integrating linear and dependent types [slides]

A video projector will be available, as well as a (modest) whiteboard. There are several smaller rooms available for break-out groups in the afternoon.

(Courtesy of Marco Gaboardi)

Jean-Yves Girard: Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987)

Philip Wadler: Is There a Use for Linear Logic? PEPM 1991: 255-273

Jean-Yves Girard, Andre Scedrov, Philip J. Scott: Bounded Linear Logic: A Modular Approach to Polynomial-Time Computability. Theor. Comput. Sci. 97(1): 1-66 (1992)

David A. Wright, Clement A. Baker-Finch: Usage Analysis with Natural Reduction Types. WSA 1993: 254-266

François Pitt: The Bounded Linear Calculus: A characterization of the class of polynomial-time computable functions based on bounded linear logic. Master thesis, 1994.

Martin Hofmann, Philip J. Scott: Realizability models for BLL-like languages. Theor. Comput. Sci. 318(1-2): 121-137 (2004)

Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong: Syntactic Control of Concurrency. ICALP 2004: 683-694

Ulrich Schöpp: Stratified Bounded Affine Logic for Logarithmic Space. LICS 2007: 411-420

Norihiro Kamide: Linear Exponentials as Resource Operators: A Decidable First-order Linear Logic with Bounded Exponentials. JELIA 2008: 245-257

Ugo Dal Lago, Martin Hofmann: Bounded Linear Logic, Revisited. TLCA 2009: 80-94

Ugo Dal Lago, Ulrich Schöpp: Functional Programming in Sublinear Space. ESOP 2010: 205-225

Ugo Dal Lago, Ulrich Schöpp: Type Inference for Sublinear Space Functional Programming. APLAS 2010: 376-391

Jason Reed, Benjamin C. Pierce: Distance makes the types grow stronger: a calculus for differential privacy. ICFP 2010: 157-168

Alberto Carraro, Thomas Ehrhard, Antonino Salibra: Exponentials with Infinite Multiplicities. CSL 2010: 170-184

Ugo Dal Lago, Marco Gaboardi: Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8(4) (2011)

Dan R. Ghica, Alex Smith: Geometry of synthesis III: resource management through type inference. POPL 2011: 345-356

Ugo Dal Lago, Barbara Petit: Linear dependent types in a call-by-value scenario. PPDP 2012: 115-126

Ugo Dal Lago, Barbara Petit: The geometry of types. POPL 2013: 167-178

Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, Benjamin C. Pierce: Linear dependent types for differential privacy. POPL 2013: 357-370

Ugo Dal Lago, Giulio Pellitta: Complexity Analysis in Presence of Control Operators and Higher-Order Functions (Long Version). CoRR abs/1310.1763 (2013)

Dan R. Ghica, Alex Smith: From bounded affine types to automatic timing analysis. CoRR abs/1307.2473 (2013)

Participant feedback [PDF]