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 complexity-bounded 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 lambda-calculus... 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 complexity-bounded 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 call-for-paper 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). Jean-Yves Marion , LORIA Nancy.


February 13 - 17, 2006



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 )



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  Jean-Yves Moyen Resource Control Graphs ( slides )
11:45 - 12:30  Karl-Heinz Niggl Certifying Polynomial Time and Linear/Polynomial Space for Imperative Programs ( slides )
12:30 - 14:00  Lunch



Linguistic and Logic and Dynamics and structures of biological networks workshops



Room: Annexe CIRM-CNRS
9:00 -10:30  Jean-Yves 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 CIRM-CNRS
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 Lambda-Calculus and Intersection Types ( slides )
16:45 - 17:30  Daniel de Carvalho Non Uniform Semantics for Lambda-Calculus, Intersection Types and Computation Time ( slides )



Room: Annexe CIRM-CNRS
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 )