![]() |
![]() |
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 listsElectromagnetic Communications and Sensing Research Seminar Series Theoretical Physics Journal Club Centre for Computational Biology Seminar SeriesOther talksGeometry of alternating projections in metric spaces with bounded curvature Quantum simulations using ultra cold ytterbium TBC Perfect matchings in random sparsifications of Dirac hypergraphs When less is more - reduced physics simulations of the solar wind Sensing and metrology activities at NPL, India |