2FC ON SATURDAY, JULY 12TH, 2014

View: session overviewtalk overviewside by side with other conferences

14:30-16:00 Session 18F

Location: FH, Dissertantenraum E104

14:30 | A cubical representation of local states ABSTRACT. 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 | Computational complexity in the lambda-calculus: what's new? ABSTRACT. 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. |

15:30 | On the parallel reduction and complexity of interaction-net systems ABSTRACT. Interaction nets form an inherently parallel computation model. We approach complexity analysis of interaction-net systems using typing and semantic interpretation techniques. |

16:30-18:00 Session 20F

Location: FH, Dissertantenraum E104

16:30 | On the Value of Variables ABSTRACT. 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. |

17:00 | Automated Complexity Analysis of Term Rewrite Systems ABSTRACT. 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 | Subrecursive Linear Dependent Types and Computational Security ABSTRACT. 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:15-19:15 Session 21

Location: FH, Dissertantenraum E104

18:15 | Proof theoretic approaches to rewriting ABSTRACT. 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. |