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.

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.

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

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.

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.

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.

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.