University of Birmingham > Talks@bham > Theoretical computer science seminar > The Functional Machine Calculus

The Functional Machine Calculus

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

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

Zoom details


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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.