Invited Speakers


Martin Hofmann (Ludwig-Maximilians-Universität München)
 Multivariate Amortized  Resource Analysis" (joint work with Jan Hoffmann and Klaus Aehlig)

We study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization, or sized types bound the resource usage or result size of such a procedure by a sum of unary functions of the sizes of the arguments.
In this paper we generalize this to arbitrary multivariate polynomial functions thus allowing bounds of the form $mn$ which had to be grossly overestimated by $m^2+n^2$ before.
 Our framework even encompasses bounds like $\sum_{i,j\leq n} m_i m_j$ where the $m_i$ are the sizes of the entries of a list of length $n$.
This allows us for the first time to derive useful resource bounds for operations on matrices that are represented as lists of lists and to considerably improve bounds on other super-linear operations on lists such as longest common subsequence and removal of duplicates from lists of lists.
 Furthermore, resource bounds are now closed under composition which improves accuracy of the analysis of composed programs when some or all of the components exhibit super-linear resource or size behavior.
The analysis is based on a novel multivariate amortized resource analysis.  We present it in form of a type system for a simple first-order functional language with lists and trees, prove soundness, and describe automatic type inference based on linear  programming.
We have experimentally validated the automatic analysis on a wide range of examples from functional programming with lists and trees. The obtained bounds were compared with actual resource consumption. All bounds were asymptotically tight, and the constants were close or even identical to the optimal ones.

Daniel Leivant (Indiana University)
Ramification and computational complexity

Ramification in logic goes back to Whitehead and Russell's Type Theory over a century ago. We make the case that ramified second order logic is an attractive master formalism for descriptive and deductive aspects of computational complexity.
    Our main technical observations have to do with ramified recurrence and corecurrence. Ramification of recurrence has been used for some time to provide implicit characterizations to computational complexity classes, in particular polynomial time. We show that ramification of recurrence can be construed as syntactic sugar for ramification in second order logic. We give a natural characterization of PTime by provability in ramified second-order logic, and report on dual characterizations for ramified corecurrence on streams.

Ricardo Peña (Universidad Complutense de Madrid)
 Certification of Polynomial Memory Bounds 
There are a number of works automatically inferring symbolic bounds for the time or memory consumed by a program. Certifying that these bounds are correct is a different matter. Certifying is important because the analyses could be unsound, or have been wrongly implemented. But the certifying process should not be necessarily tied to the method used to infer those bounds. Although the motivation for the work presented here is certifying the memory bounds inferred by our compiler, we have developed a certifying method which could equally be applied to bounds computed by hand.

The certification process is divided into two parts: (a) an off-line part consisting of proving the soundness of a set of proof rules. This part is independent of the program being certified, and its correctness is established once forever by using the proof assistant  Isabelle/HOL; and (b) a compile-time program-specific part in which the proof rules are applied to a particular program and their premises proved correct.  For the second part, we use a mathematical tool for proving instances of the Tarski decision problem on quantified formulas in real closed fields.