July 12, 2014

Session 1
14:30 – 15:00 Paul-André Melliès (PPS)
A cubical representation of local states

In this talk, I will explain how imperative programs with local stores may be represented as cubes living inside types themselves represented as cubical sets. I will illustrate with a few examples how this geometric representation of programs with states should help us to reason about resource allocation and deallocation in imperative programs. This is joint work with Kenji Maillard.

15:00 – 15:30 Beniamino Accattoli (University of Bologna)
On the Value of Variables

Call-by-value and call-by-need lambda-calculi are defined using the distinguished syntactic category of values. In theoretical studies, values are variables and abstractions. In more practical works, values are usually defined simply as abstractions. This paper shows that practical values lead to a more efficient process of substitution---for both call-by-value and call-by-need---once the usual hypothesis for implementations hold (terms are closed, reduction does not go under abstraction, and substitution is done in micro steps, replacing one variable occurrence at the time). Namely, the number of substitution steps becomes linear in the number of beta-redexes, while theoretical values only provide a quadratic bound.

15:30 – 16:00 Stéphane Gimenez (University of Innsbruck)
On the parallel reduction and complexity of interaction-net systems

Interaction nets form an inherently parallel computation model. We approach complexity analysis of interaction-net systems using typing and semantic interpretation techniques.

16:00–16:30 Coffee Break

Session 2
16:30 – 17:00 Damiano Mazza (Paris 13)
Computational complexity in the lambda-calculus: what's new?

The lambda-calculus models computation via substitution, an abstract notion whose concrete meaning in terms of elementary computational steps is unclear a priori. As a consequence, the model of choice for computational complexity is usually some variant of Turing machines, even in the higher-order case (which seems regretful, given the functional nature of the lambda-calculus). In recent years, a number of tools related to linear logic (proof nets, explicit substitutions, linear calculi) have provided us with a finer understanding of the substitution process, offering new perspectives on the relationship between lambda-calculus and computational complexity. In this talk, I will survey three specific cases: Accattoli and Dal Lago's invariance result for beta-reduction; an ongoing work by Dal Lago and myself proposing a new formulation of higher-order complexity entirely based on a lambda-calculus; and some of my results and ongoing work on characterizing non-uniform circuit complexity classes with infinitary lambda-terms.

17:00 – 17:30 Martin Avanzini (University of Bologna)
Automated Complexity Analysis of Term Rewrite Systems

TcT, the Tyrolean complexity tool, is a tool for automatically proving polynomial upper bounds on the runtime complexity of term rewriting systems. In this talk, I will briefly outline the formal framework and main techniques underlying TcT.

17:30 – 18:00 Ugo Dal Lago (University of Bologna)
Subrecursive Linear Dependent Types and Computational Security

Various techniques for the complexity analysis of programs have been introduced in the last twenty years, spanning from type systems, to abstract interpretation, to path orders. A peculiar approach consists in adopting linear dependent types, which have been proved to be a relative complete methodology for complexity analysis. We here study linear dependency in a subrecursive setting, where recursion is structural. On the one hand, we show that linear dependent types are robust enough to be adaptable, by way of effects, to a language with imperative features. On the other, we show the obtained system to be enough powerful to type nontrivial examples drawn from computational security, which is the driving motivation for this work.

18:00–18:15 Short Break

Session 3
18:15 – 18:45 Thomas Powell (IHES Paris)
Proof theoretic approaches to rewriting

A key method for establishing the termination or complexity of a program in some high level language is to capture its salient features in an abstract rewrite system which can then be analysed separately. In this talk I will discuss some of the deep links between rewriting theory and classical proof theory, in particular how powerful techniques from proof theory can be used to derive the complexity of rewrite systems and shed light on well-known tools such as recursive path orderings. My aim is ultimately to present some proof theoretic ideas for understanding and analysing rewrite systems.

Workshop Dinner
20:00– Café Rüdigerhof, Hamburgerstraße 20, 1050 Wien