The area of Implicit Computational Complexity (ICC) has grown out from several proposals to use
logic and formal methods to provide languages for complexity-bounded computation
(e.g. Ptime, Logspace computation). It aims at studying computational complexity without referring
to external measuring conditions or a particular machine model, but only by considering language
restrictions or logical principles implying complexity properties.
This workshop focuses on ICC methods related to programs (rather than descriptive methods). In
this approach one relates complexity classes to restrictions on programming paradigms
(functional programs, lambda calculi, rewriting systems), such as ramified recurrence, weak
polymorphic types, linear logic and linear types, and interpretative measures. The two main
objectives of this area are:
- to find natural implicit characterizations of various complexity classes of functions, thereby
illuminating their nature and importance;
- todesign methods suitable for static verification of program complexity.
Therefore ICC is related on the one hand to the study of complexity classes, and on the other hand to
static program analysis. The workshop will be open to contributions on various aspects of ICC
including (but not exclusively):
- types for controlling complexity,
- logical systems for implicit computational complexity,
- linear logic,
- semantics of complexity-bounded computation,
- rewriting and termination orderings,
- interpretation-based methods for implicit complexity,
- programming languages for complexity-bounded computation,
- application of implicit complexity to other programming paradigms (e.g. imperative or object-oriented languages).
The first two DICE workshops were held in 2010 in Cyprus and in 2011 in Germany, both
as part of ETAPS conferences. Before that, several meetings on this topic had already been held
with success in Paris (WICC 2008), and Marseille (GEOCAL 2006 workshop on Implicit computational complexity).