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 - 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.
- Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
- Meeting ID: 818 7333 5084
- Passcode: 217
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. |
## Other listsElectromagnetic Communications and Sensing Research Seminar Series Theoretical Physics Journal Club Centre for Computational Biology Seminar Series## Other 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 |