The Functional Machine Calculus

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

• Chris Barrett (University of Birmingham)
• Friday 28 October 2022, 13:30-14:20
• LG23, SoCS and Zoom (see abstract for link).

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

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

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:

• 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.