Highlights Conference 2014 Conference Abstract
Turing machines and lambda-calculus were the first two approaches to define computability. In verification the Turing machine approach is predominant: finite automata, counter machines, pushdown automata, multi-pushdown automata, etc. Typing disciplines are another approach to program correctness. Rich types can express a variety of program properties, as for example that a list is sorted, or that resources are accessed. In typing disciplines the lambda approach is paramount. The perspectives of verification and typing are different. One seldom types a pushdown automaton; similarly it is not yet common to consider lambda terms as machines. In this talk we argue that the latter is not only quite natural, but also useful. Simply typed lambda-calculus with fixpoints is an abstraction of higher-order functional programs. It faithfully models the control in such programs but abstracts from data: all constants are non-interpreted. In particular, terms of this calculus can encode finite automata so that an evaluation of a term gives the behaviour of the automaton it encodes (a regular tree). In a similar way terms can encode pushdown automata. Lambda-calculus comes with its methods of evaluation that do not rely on pushdowns. This gives a new perspective on the so called pushdown hierarchy: automata with higher-order stacks. For example, Muchnik's theorem stating the compatibility of some graph unfoldings with MSOL finds a new explanation in this context. Lambda-calculus has a richer syntax that allows naturally to talk about contexts, multi-contexts, higher-order contexts etc. Lambda-calculus comes with models that make it possible to understand better the invariants of computation. In summary, simply typed lambda-calculus with recursion offers new questions that, also for reasons of perspective, were not considered by the typing community. 15: 30 15: 45 Coffee Break