We show how the complexity of higher-order functional programs can be analysed
automatically by applying program transformations to a defunctionalised versions of them …

In this paper, we present a variant of the dependency pair method for analysing runtime
complexities of term rewrite systems automatically. This method is easy to implement, but …

Whether the number of β-steps in the λ-calculus can be taken as a reasonable time cost
model (that is, polynomially related to the one of Turing machines) is a delicate problem …

In this paper we present a combination framework for the automated polynomial complexity
analysis of term rewrite systems. The framework covers both derivational and runtime …

In CSL-LICS 2014, Accattoli and Dal Lago [1] showed that there is an implementation of the
ordinary (ie strong, pure, call-by-name) λ-calculus into models like RAM machines which is …

This paper introduces a new methodology for the complexity analysis of higher-order
functional programs, which is based on three ingredients: a powerful type system for size …

The lambda-calculus is a widely accepted computational model of higher-order functional
programs, yet there is not any direct and universally accepted cost model for it. As a …

We study the termination problem for probabilistic term rewrite systems. We prove that the
interpretation method is sound and complete for a strengthening of positive almost sure …

This paper introduces the exponential substitution calculus (ESC), a new presentation of cut
elimination for IMELL, based on proof terms and building on the idea that exponentials can …

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can
simulate each other within a polynomially overhead in time. Is lambda-calculus a …