Quantitative techniques are emerging in different areas of computer science, such as model checking, logic, automata theory, and programming languages, to meet the challenge of resource-aware computations.
In this talk, we discuss multi-types, also known as non-idempotent (intersection) types, which provide a natural tool for reasoning about resource consumption in higher-order languages. Multi-types are applicable to a wide range of powerful models of computation, such as pattern matching, control operators and infinite computations.
We survey some recent semantic and operational results in the domain.