Bounded Linear Logic Workshop

Fontainebleau, 2-4 December 2013

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

Participants to the BLL workshop

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.


(morning talks and time to work in smaller groups in the afternoons)

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.

A BLL Reader

(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]