University of Birmingham > Talks@bham > Theoretical computer science seminar > Implicit automata in typed λ-calculi

Implicit automata in typed λ-calculi

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George Kaye.

Zoom details


The proofs-as-programs correspondence involves programming languages which are terminating, hence Turing-incomplete. What predicates or functions do the terms of some appropriate type (think of “string → bool”) in such a language define? The field of Implicit Computational Complexity has shown that interesting complexity classes could be characterised this way. Such results tend to rely on type systems deliberately engineered for this purpose, often inspired from linear logic.

In the work presented here, we consider on typed λ-calculi (some of which are linear or affine) whose original “raison d’être” is unrelated to questions of expressive power. We contend that connections with finite-state computation, i.e. automata theory, then arise more naturally in this context than with computational complexity. In particular, this talk will focus on transducers, that is, automata that can produce output strings. If time allows, I will also talk about a characterisation of star-free languages using a non-commutative (planar) λ-calculus, and/or some of the category-theoretic technology that we deploy in our proofs.

This is joint work with Pierre Pradic (Lecturer at Swansea University), and a more technical summary of our work can be found at

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.