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
- Patrick Baillot, Erika De Benedetti and Simona Ronchi Della Rocca
Characterizing polynomial and exponential complexity classes in elementary lambda-calculus - Brian Redmond
Soft Linear Logic and the Polynomial Hierarchy
12:30–14:00 Lunch
14:15–15:15 Invited Talk
15:15–16:00 Session 2: Term Rewriting
-
Martin Avanzini and Naohi Eguchi
A New Term Rewriting Characterisation of ETIME functions
16:00–16:30 Coffee Break
16:30–17:15 Session 3: Lambda Calculus
-
Beniamino Accattoli and Ugo Dal Lago
Beta Reduction is Invariant, Indeed
Sunday, April 6
9:30–10:30 Invited Talk
10:30–11:00 Coffee Break
11:00–12:30 Session 4: Program Analysis
-
Michael Schaper
A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems -
Mauro Piccolo, Claudio Sacerdoti Coen and Paolo
Tranquilli
The labelling approach to precise resource analysis on the source code, revisited
12:30–14:15 Lunch
14:15–15:15 Invited Talk
15:15–16:00 Session 5: Context Semantics
-
Matthieu Perrinel
Context semantics for interaction nets
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:
- to find natural implicit characterizations of various complexity classes of functions, thereby illuminating their nature and importance;
- to design methods suitable for static verification of program complexity.
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):
- 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
- theoretical foundations of program complexity analysis
- theoretical foundations of program complexity analysis
- application of implicit complexity to security
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.
Submission
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.
Sponsors
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.
