DICE is a thematic workshop in the field of Implicit Computational Complexity, where researchers in the area can meet and discuss their most recent results. It takes place annually as part of ETAPS.

Workshop Program

Saturday, April 5

9:30–10:30 Invited Talk

10:30–11:00 Coffee Break

11:00–12:30 Session 1: Linear Logic

12:30–14:00 Lunch

14:15–15:15 Invited Talk

15:15–16:00 Session 2: Term Rewriting

16:00–16:30 Coffee Break

16:30–17:15 Session 3: Lambda Calculus

Sunday, April 6

9:30–10:30 Invited Talk

10:30–11:00 Coffee Break

11:00–12:30 Session 4: Program Analysis

12:30–14:15 Lunch

14:15–15:15 Invited Talk

15:15–16:00 Session 5: Context Semantics

16:00–16:30 Coffee Break

16:30–17:30 Business Meeting

Scope and Topic

The area of Implicit Computational Complexity (ICC) has grown from several proposals for using logic and formal methods to provide languages for complexity-bounded computation (e.g. PTIME, LOGSPACE computation). Its aim is to study computational complexity without reference to external measuring conditions or particular machine models, but only in terms of language restrictions or logical/computational 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:

Therefore ICC is related on 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):

Invited Talks

Dan Ghica

Resource control via bounded linear typing

Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. We introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This is a useful type-theoretic and denotational framework for resource-sensitive compilation, and it represents a generalization of several existing type systems. As a nontrivial instance, motivated by hardware compilation, we present a new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.

Akitoshi Kawamura

Applying higher-type complexity to analysis

Computable Analysis studies problems involving real numbers from the viewpoint of computability and complexity, and provides a foundation for numerical algorithms with validated precision. Higher-type complexity classes are often useful in this context, since real numbers, real functions and operators on real functions are by nature specified by approximation in an interactive manner. In this talk, I will introduce how we formulate and study computational complexity in analysis, with examples of operators that belong to, or are complete for, type-two (or higher) classes PSPACE, NP, P, NC, etc.

Damiano Mazza

Non-Uniform Polytime Computation in the Infinitary Affine Lambda-Calculus

We will present an implicit, functional characterization of the class of non-uniform polynomial time languages, based on an infinitary affine lambda-calculus and on previously defined bounded-complexity subsystems of linear (or affine) logic. The fact that the characterization is implicit means that the complexity is guaranteed by structural properties of programs rather than explicit resource bounds. As a corollary, we obtain a proof of the (already known) P-completeness of the normalization problem for the affine lambda-calculus which mimics in an interesting way the proof of the Cook-Levin theorem. This suggests that the relationship between affine and usual lambda-calculus is deeply similar to that between Boolean circuits and Turing machines.

Georg Moser

Automated Complexity Analysis Based on the Dependency Pair Method

This talk is concerned with automated complexity analysis of term rewrite systems. I will present variants of the dependency pair method for analysing runtime complexities of rewrite systems automatically: the weak dependency pair method and the dependency tuple method. Furthermore I will link to related notions in ICC and report on very recent results on the use of context-sensitive rewriting in complexity analysis.


Authors are invited to submit an extended abstract of up to 5 pages by January 5, 2014 to the DICE 2014 EasyChair page.

Abstracts must be written in English and be submitted as a single PDF file.

Submissions will be judged on originality, relevance, interest and clarity. Accepted abstracts will be presented at the workshop. Preference will be given to abstracts describing work (including work in progress) that has not been published elsewhere before the workshop. Any previous publication or submission of submitted work should be clearly indicated in the submission.

The workshop will not have formal proceedings and is not intended to preclude later publication at another venue.

Submissions of abstracts by PC members are allowed and encouraged.


The workshop is kindly supported by GDR Informatique Mathématique, ANR JCJC project Coquas, and DFG project Purple.

Previous Workshops and Special Issues

Information about previous instances of the workshop and special issues of journals can be found at the homepage of the DICE workshop series.

Invited Speakers

Important Dates

Abstract Submission
January 5, 2014
January 20, 2014
April 5-6, 2014

Program Committee

Steering Committee


Call for Papers: txt, pdf

Background: View of Alps from Grenoble
Impressum – Legal Notice