![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Implicit automata in typed λ-calculi
Implicit automata in typed λ-calculiAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact George Kaye. Zoom details
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:
Note that ex-directory lists are not shown. |
Other listsMetamaterials and Nanophotonics Group Seminars School of Mathematics events Topology and Dynamics seminarOther talksThe tragic destiny of Mileva Marić Einstein Ultrafast Spectroscopy and Microscopy as probes of Energy Materials TBA Quantum Sensing in Space Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy Life : it’s out there, but what and why ? |