![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > The Functional Machine Calculus
The Functional Machine CalculusAdd 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 Functional Machine Calculus (FMC) was recently introduced by Heijltjes [1] as a generalization of the lambda-calculus to include higher-order global state, probabilistic and non-deterministic choice, and input and ouput, while retaining confluence. The calculus can encode both the call-by-name and call-by-value semantics of these effects. This is enabled by two independent generalizations. The first decomposes the syntax of the lambda-calculus in a way that allows for sequential composition of terms and the encoding of reduction strategies. The second paramaterizes application and abstraction in terms of `locations’, which gives a unification of the operational semantics, syntax, and reduction of the given effects with those of the lambda-calculus. The FMC further comes equipped with a simple type system which restricts and captures the behaviour of effects, and guarantees strong normalisation. This talk will introduce the FMC and give a summary of its categorical semantics. In particular, an equational theory is introduced, and shown to be validated by a notion of observational equivalence. The category of closed FMC -terms modulo this theory, with composition given by sequencing, then forms the free Cartesian closed category. Thus another good property of the lambda-calculus is preserved by the FMC . [1] Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus. June 2022. 38th International Conference on Mathematical Foundations of Programming Semantics, MFPS 2022 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 listsType the title of a new list here Bham Talks Type the title of a new list hereOther talksQuantum simulations using ultra cold ytterbium Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Geometry of alternating projections in metric spaces with bounded curvature Extending the Lax type operator for finite W-algebras TBC CANCELLED: An overview of Non-Reductive Geometric Invariant Theory and its applications |