Workshop on
Implicit Computational Complexity
as part of GEOCAL'06
Marseille  Luminy
February 13  17, 2006
NEW: CFP, Special Issue of ACM ToCL on
Implicit Computational Complexity.
Context: This workshop is part of Geometry of Computation 2006 (Geocal06), a special series of
events in theoretical computer science organized by the GEOCAL group and taking place
at the CIRM from January 30 to March
3.
Geocal06 is supported by the following institutions: CIRM, CNRS, Luminy, ParisNord, FRUMAM,
IML, PPS, LIPN.
Programme (with Slides of the talks) and Abstracts .
Invited speakers:
Timetable of the week (3 workshops)
Presentation:
Implicit Computational Complexity (ICC) has emerged from various propositions
to use logic and formal methods like types, rewriting systems... to provide
languages for complexitybounded computation, in particular for polynomial time
computing.
It aims at studying the computational complexity of programs without refering
to a particular machine model and explicit bounds on time or memory, but instead
by relying on logical or computational principles that entail complexity
properties. Several approaches have been explored for that purpose, like linear
logic, restrictions on primitive recursion, rewriting systems, types and
lambdacalculus... They often rely on the functional programming paradigm.
Two objectives of ICC are:
 on the one hand to find natural implicit logical characterizations of
functions of various complexity classes,
 on the other hand to design systems suitable for static verification of
programs complexity.
In particular the latter goal requires characterizations which are general
enough to include commonly used algorithms.
This meeting will be preceded by a
course on Complexity and Logic (6>10/2)
organized as part of the GEOCAL'06 winter school and especially targeted at PhD
students, with lectures by P.Baillot, M.Hofmann and J.Y. Marion. Some
(limited) funding is possible for students attending the school and/or the
workshop.
The workshop is intended to be a forum for researchers interested in
ICC to discuss recent developments and open issues. It will be open to
contributions on various aspects of ICC including (but not exclusively):
 logical systems for implicit computational complexity,
 linear logic,
 semantics of complexitybounded computation,
 rewriting and termination orderings,
 types for controlling complexity,
 extensions from functional approach to ICC to imperative or concurrent
setting; applications to automated verification...
Propositions of contributions consist in a title and a short abstract (see the
Geocal06 site ).
After the workshop a callforpaper for a special issue of a journal might be
considered (either for the GEOCAL'06 session, or for the workshop itself), with
standard refering procedure.
Preregistration: on the Geocal06 site. Deadline: October 30,
2005.
Organizers:
Patrick Baillot
, LIPN, Univ. Paris 13/CNRS,
(contact).
JeanYves Marion , LORIA Nancy.
Programme
February 13  17, 2006
Monday 
13/2 

Room 
Salle de conférence CIRM 

9:00  10:30 
Martin Hofmann 
Programming Languages for LOGSPACE
( slides ) 
10:30  11:00 
Coffee break 
11:00  11:30 
Reinhard Kahle 
Towards an Implicit Characterization of NC^k
( slides ) 
11:30  12:15 
Frédéric Dabrowski 
Feasible Reactivity for Synchronous Cooperative threads
( slides )




12:30  14:00 
Lunch 


Room: 
Salle de conférence CIRM 
14:00  14:45 
Vincent Atassi 
Type Inference in Elementary Linear Logic with Coercions and its Implementation
( slides )

14:45  15:30 
Paolo Tranquilli 
The Typing Problem for Second Order Light Logics
( slides ) 
15:30  16:00 
Coffee break 
16:00  16:45 
Paulin de Naurois 
A Measure of Space for Computing over the Reals
( slides ) 
16:45  17:30 
Emmanuel Hainry 
Recursive Analysis and Real Recursive Functions
( slides ) 

Tuesday 
14/2 

Room: 
Salle de conférence CIRM 
9:00  10:30 
James Royer 
Adventures in Time and Space
( slides ) 
10:30  11:00 
Coffee break 
11:00  11:45 
JeanYves Moyen 
Resource Control Graphs
( slides ) 
11:45  12:30 
KarlHeinz Niggl 
Certifying Polynomial Time and Linear/Polynomial Space for Imperative Programs
( slides ) 



12:30  14:00 
Lunch 

Wenesday 
15/2 



Linguistic and Logic and Dynamics and structures of biological networks workshops


Thursday 
16/2 

Room: 
Annexe CIRMCNRS 
9:00 10:30 
JeanYves Girard 
Finiteness and Hyperfiniteness and Light Exponentials
( slides .ps ) 
10:30  11:00 
Coffee break 
11:00  11:45 
Ugo Dal Lago 
Context Semantics, Linear Logic and Implicit Complexity
( slides ) 
11:45  12:15 
Ulrich Schöpp 
Space Efficiency and the Geometry of Interaction
( slides ) 



12:30  14:00 
Lunch 

Room: 
Annexe CIRMCNRS 
14:00  15:30 
Kazushige Terui 
Intersection Types for Implicit Computational Complexity
( slides ) 
15:30  16:00 
Coffee break 
16:00  16:45 
Simona Ronchi della Rocca 
Soft Linear LambdaCalculus and Intersection Types
( slides )

16:45  17:30 
Daniel de Carvalho 
Non Uniform Semantics for LambdaCalculus, Intersection Types and
Computation Time
( slides )

Friday 
17/2 

Room: 
Annexe CIRMCNRS 
12:30  14:00 
Lunch 

14:00  14:45 
Harry Mairson 
MLL Normalization and Transitive Closure: Circuits, Complexity and Euler Tours
( slides ) 
14:45  15:30 
Isabel Oitavem 
Pointers and Polynomial Space Functions
( slides ) 
15:30  16:00 
Coffee break 
16:00  16:45 
Lorenzo Tortora de Falco 
Obsessional Cliques: a Semantic Characterization of Bounded Time Complexity
( slides ) 
16:45  17:15 
Brian Redmond 
Categorical Models of SLL and Ptime Computation
( slides ) 
Abstracts
 Vincent Atassi , LIPN, Université Paris 13, France.
Title: Type inference in Elementary Linear Logic with coercions and its implementation
Abstract:
Elementary Linear Logic (ELL), is a logic in which proofs reduce to their normal
form by cutelimination in elementary time. Conversely, this system is expressive
enough to encode all elementary functions from integers to integers and thus, yields
an implicit and logic characterisation of the elementary time complexity class. Using
the CurryHoward correspondence, we focus on the use of ELL as type system for lambda
calculus, and more precisely, on type inference. Looking at ELL proofnets, the bounded
termination properties arise from a certain discipline in placing boxes. Specifically,
since some linear logic principles are not valid in ELL, a function cannot be applied
to an argument if both terms are not at the same box nesting level. However, data types
(such as integers) may admit coercions, that is the possibility to add boxes and increase
nesting level, and from a typing point of view, that means the !^n N o !^(n+1)N
formula has a proof. To ensure typing of some basic functions such as square elevation, the
programmer should explicitly place those coercions in his terms, and that is not satisfactory,
for it breaks the transparency of typing. We will present an efficient type inference algorithm
for ELL, and discuss its implementation in caml. Next we will introduce its extension to the
automatic coercions placement, using a subtyping relation, which as a result correctly extends
the set of typable terms.
 Daniel de Carvalho , IML Université AixMarseille II, Marseille, France.
Title: Non uniform semantics for Lambda Calculus, intersection types
and computation time
Abstract:
The relational semantics for Linear Logic induces a semantics
for the type free Lambda Calculus. This is built on nonidempotent
intersection types and we prove that the size of the derivations is
related to the execution time of lambdaterms in the Krivine machine.
 Frédéric Dabrowski, INRIA Sophia Antipolis, France.
Title: Feasible reactivity for synchronous cooperative threads
Abstract:
We are concerned with programs composed of cooperative threads whose
execution proceeds in synchronous rounds called instants. We develop static analysis
methods to guarantee that
each instant terminates in time polynomial in the size of the parameters
of the program at
the beginning of the computation.
 Ugo Dal Lago , Università di Bologna, Italy.
Title: Context Semantics, Linear Logic and Implicit Complexity
Abstract:
We study context semantics of (multiplicative) linear logic
in view of implicit complexity issues. In particular, we show how
semantics can be used to give bounds on the normalization time for any linear
logic proofnet.
 JeanYves Girard, IML CNRS Marseille, France.
Title:
Hyperfiniteness and light exponentials
Abstract:
Light exponentials are based upon the idea of termination
a priori, independently of logical correctness. This is the case for perfect
logic due to the finite dimension of the spaces involved. In presence of
exponentials, one needs an infinite space, but not too infinite so too speak,
infinite from outside, finite from inside. The vN algebra of a locally finite
discrete group is likely to answer the problem. Everything can be handled by
finite matrices, but of arbitrary sizes. Although there is only one hyperfinite
algebra of this form, the finite approximants seen as syntax will look very
depending on the group. A specific group, basically devoted to the drawing of
links and boxes is therefore at work.
 Emmanuel Hainry , LORIA/INPL, Nancy.
Title:Recursive analysis and real recursive functions
Abstract:
From the beaver to the tortoise, every living being
likes to compute, and uses its own model of computing. The most widespread
and accepted computation paradigm deals with integer numbers and works in
discrete time. This behaviour is embodied by Turing machines, supported by
ChurchTuring thesis that states that all reasonable discrete models of computation
compute exactly the same class of functions : the computable functions. However
computing can be done in continuous time and over continuous domains. Some machines
working in this framework have been built an dused. Several different models have
been created to describe such computation. Unfortunately, there exist few comparisons
between these models (and most results are of inequality). Among those models, let us
cite computable analysis that relies on type2 machines which are more or less
Turing machines that work on a sequence representing a real number and output a
similar sequence, the General Purpose Analog Computer (proposed by Shannon) which
puts together ``real'' computation units in circuits and realrecursive functions
that mimics the definition of discrete computable functions as a closure. This work's
aim is to exhibit a bridge between computable analysis and real recursive functions.
This way, we provide algebraic characterizations of some classes of functions from
computable analysis.
 Martin Hofmann, LMU Munich, Germany.
Title
Programming Languages for LOGSPACE
Abstract:
Joint work with Jan Johannsen and Uli Schöpp. I will describe
existing logical and linguistic formalisms capturing LOGSPACE or subclasses thereof
and outline a tentative research programme aimed at isolating PTIME from a natural
subset of LOGSPACE that contains popular LOGSPACE algorithms (but not Reingold's algorithm!)
 Paulin Jacobé de Naurois, LIPN, Université Paris 13, France.
Title:
A Measure of Space for Computing over the Reals
Abstract:
We propose a new complexity measure of space for the BSS model of computation.
We define LOGSPACE_W and PSPACE_W complexity classes over the reals. We prove
that LOGSPACE_W is included in NC^2_R and in P_W, i.e. is small enough for
being relevant. We prove that the Real Circuit Decision Problem is
P_Rcomplete
under LOGSPACE_W reductions, i.e. that LOGSPACE_W is large enough for
containing
natural algorithms. We also prove that PSPACE_W is included in PAR_R.
 Reinhard Kahle, Departamento de Matemática, Universidade de Coimbra, Portugal.
Title:
Towards an implicit characterization of NC^k
Abstract:
We report on work in progress about an implicit characterization of NC^k.
This is joint work with Guillaume Bonfante, JeanYves Marion, and Isabel Oitavem
 Harry Mairson, Brandeis University, USA.
Title
MLL normalization and transitive closure: circuits, complexity, and Euler
tours
Abstract:
 JeanYves Moyen, LIPN, Université Paris 13, France.
Title:
Resource Control Graphs
Abstract:
Several programs analysis can be seen as annotation on some kind of Control
Flow Graphs, thus describing properties of termination, time or space
complexity. In order to try and unify them all, I introduce the notion of
Resource Control Graph, based on the tool of Resource Systems with States, a
generalisation of Petri nets. This allows to represent in a comprehensive way
several existing
analysis.
 KarlHeinz Niggl, Technische Universität Ilmenau, Germany.
Title:
Cerifying polynomial time and linear/polynomial space for imperative programs
Abstract:
.pdf
 Isabel Oitavem, Universidade Nova de Lisboa, Portugal.
Title:
Pointers and polynomial space functions
Abstract:
In this talk, we give an implicit characterization
of the class of functions computable in polynomial space by deterministic
Turing machines  Pspace. This is a characterization in the vein of the
BellantoniCook characterization of the polytime functions, Ptime, given in
[BC]. The main difference between these two characterizations is the
formulation of the recursion scheme. To reach Pspace one introduces pointers
in the recursion scheme.
[BC] S. Bellantoni and S. Cook, A new recursiontheoretic
characterization of polytime functions, Computational Complexity, 2:97100, 1992
 Brian Redmond, University of Ottawa, Canada.
Title:
Multiplexor Categories and Models of Soft Linear Logic
Abstract:
We begin with an introduction to soft linear logic (SLL) and the
corresponding notion of multiplexor category. A multiplexor category consists of a
symmetric monoidal closed category (SMCC) together with a soft exponential
operator ! and monoidal natural transformations called multiplexors. We shall see
that a multiplexor category provides a denotational semantics for SLL. Next we
consider various ways of constructing a multiplexor category from a symmetric monoidal
closed category having countable limits, which leads to a large class of models. More
generally, we give a categorical construction (completion) for building a multiplexor
category from a SMCC having only a bounded form of multiplexing. As an application to
illustrate these ideas, we construct a realizability model for SLL based on the
HofmannScott model for BLL. Finally, we discuss connections with Baillot's Stratified
Coherence Spaces for LLL and other future work.
 Simona Ronchi della Rocca, Università di Torino, Italy.
Title:
Soft Linear Logic, lambdacalculus
and Intersection Types
Abstract:
A type assignment system is presented, assigning to terms of lambdacalculus formulas
of Lafont's Soft Linear Logic. The aim is to allow the use of $\lambda $calculus as programming
language, where types are used to assure the termination of a program in polynomial time. In order
to inherit all the good properties of the logic, a natural approach would be to transform it into
a type assignment system using the CurryHoward correspondence. Clearly the application of such
a correspondence in this case cannot be standard, since the modal connective (!) of the
logic does not have a corresponding syntactic constructor in lambdacalculus.
The resulting system does not enjoy the subject reduction property.
This lack depends on the fact that the logic is presented in a sequent calculus formulation.
We solve the problem by restricting both the set of formulas that can be used as types and
some rules of the logic, in particular
the cut rule. The result is that the set of type assignment derivations corresponds
(through the CurryHoward
correspondence) to a proper subset of the Soft Linear Logic proofs. But there is not loss in
expressiveness: we prove that the set of terms that can be typed in the restricted system is the
same as in the whole system. The restricted system enjoys the subject reduction property, and
inherits all the good properties of the Soft Linear Logic: confluence, and polynomial time
termination. Polynomial time completeness can be reached through either the use of the universal
quantification or by enriching the language by a set of constants with a suitable functional
behaviour.
Moreover by allowing a (restricted form) of intersection as type constructor, the set of algorithms
that can be written in the typed language increases, while preserving the complexity limit.
A language built from Soft Linear Logic through the CurryHoward
correspondence has been recently designed by Baillot and Mogbil. Their language preserves all
the good properties of the logic, but, in order to do so, it remembers in its syntax all the
applications of typing rules. We think that programming in the stardard lambdacalculus
is more natural and friendly.
 James Royer, Syracuse University, USA.
Title:
Adventures in Time and Space
Abstract:
We discuss what is essentially a callbyvalue version of PCF
under a complexitytheoretically motivated type system. The programming formalism,
ATR, has its firstorder programs characterize the polytime computable functions, and
its secondorder programs characterize the type2 basic feasible functionals of Mehlhorn
and Cook and Urquhart. (The ATRtypes are confined to levels 0, 1, and 2.) The type system
comes in two parts, one that primarily restricts the sizes of values of expressions and a
second that primarily restricts the time required to evaluate expressions. The sizerestricted
part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of
polytime. The timerestricting part is an affine version of Barber and Plotkin's DILL. Two
semantics are constructed for ATR. The first is a pruning of the naive denotational
semantics for ATR. This pruning removes certain functions that cause otherwise feasible forms
of recursion to go wrong. The second semantics is a model for ATR's time complexity
relative to a certain abstract machine. This model provides a setting for complexity recurrences
arising from ATR recursions, the solutions of which yield secondorder polynomial time
bounds. The timecomplexity semantics is also shown to be sound relative to the costs of
interpretation on the abstract machine
 Ulrich Schöpp, LMU Munich, Germany.
Title:
Spaceefficiency and the Geometry of Interaction
Abstract:
I will report on work in progress on using the Geometry of
Interaction for the spaceefficient evaluation of programs. MøllerNeergaard
and Mairson have recently defined the function algebra BC^_epsilon and have shown
that it captures LOGSPACE. We propose to use the Geometry of Interaction as a tool
for extending this result to more convenient programming languages and to related
complexity classes. Using the Geometry of Interaction, computation can be described
in terms of question/answerpassing on a static network. Since questions and answers
can often be stored using little space, this description can help in devising
spaceefficient ways of evaluating programs. The main purpose of this talk is to
describe how the Geometry of Interation can be used for compiling BC^_epsilonexpressions
into LOGSPACEprograms, and how it can guide the extension of BC^_epsilon.
 Kazushige Terui, NII Tokyo, Japan.
Title:
Intersection types for implicit computational complexity
Abstract:
Intersection types have proven to be useful for reducing dynamic
properties of lambdaterms (eg. normalizability) to static ones (eg. typability).
By considering their linear/affine analogues, it is possible to characterize even
finer dynamic properties, such as normalizability within a given resource bound. In
this talk, we overview some basic results on linear/affine intersection type systems,
and discuss their possible applications in implicit computational complexity.
 Lorenzo Tortora de Falco, Universita Roma Tre, Italy.
Title:
Obsessional cliques: a semantic characterization of bounded time complexity.
Abstract:
We introduce the notion of obsessional clique and prove that the
semantics of a proofnet is an obsessional clique iff the (normal form of the)
proofnet belongs to ELL.
 Paolo Tranquilli, Universita Roma Tre, Italy.
Title:
The typing problem for second order light logics
Abstract:
One of the approaches to Implicit Computational Complexity
consists in using the resource limitations built in Girard's Linear Logic to
design type theories which enforce complexity constraints on underlying
lambdaterms and which are expressive enough to exhaust the respective
complexity classes. In particular we concentrated on EALogic, which enforces
and encodes elementar functions, and LAL, together with its variant DLAL by
Baillot and Terui, which does the same with polytime functions. Questions
arise as to decidability of two problems pertaining type assiginment within
these systems: type checking (TC) consists in whether a given type can be
assigned to a given term, typability (TYP) in whether a given term can be
assigned a type at all. These problems have great importance in an eventual
implementation of such systems as programming disciplines. TC and TYP have
been proved decidable for the quantifierfree versions of these systems, but
second order has a paramount role in obtaining their expressive power.
TC is proved to be undecidable for all these systems by an adaptation of the
same result for system F by Wells, while decidability of TYP remains up to
now an unsolved problem.