Implicit automata in typed λ-calculi

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

• Lê Thành Dũng Nguyễn (École Polytechnique)
• Friday 01 April 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

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

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

Abstract

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 https://cs-web.swan.ac.uk/~pierrepradic/smp-abstract.pdf

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

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, SoCS and Zoom (see abstract for link)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.