LFCS Seminar: Tuesday 11 March: Willem Heijltjes Speaker: Willem Heijltjes Title: The Functional Machine Calculus Abstract: The Functional Machine Calculus (FMC) is a new approach to combining the lambda-calculus with computational effects, along similar lines as Moggi's monadic approach, Levy's call-by-push-value, and Plotkin and Pretnar's effect handlers. Its point of departure is to view the lambda-calculus as a simple instruction language for a call-by-name stack machine in the style of Krivine, where application pushes its argument and abstraction pops. The FMC then consists of three extensions. The first is to allow multiple independent stacks, which are then used to model higher-order store, input/output, and probabilistic choice (as a probabilistically generated stream). The second is to introduce imperative sequencing and skip, modelled through a standard continuation stack, which allows to encode call-by-value as well as the computational metalanguage and call-by-push-value. The third is to take imperative skip, which represents successful termination, and parameterize it to model exceptions as well. Sequencing is made conditional accordingly, and a natural notion of loop is introduced. This allows to further capture exception handling, constants, data types, and while-loops. With this approach, key features of the lambda-calculus extend to imperative programming. The abstract machine allows to derive a confluent notion of reduction, extending beta-reduction, and a notion of simple types that (in the absence of iteration) guarantees termination of the machine. Mar 11 2025 16.10 - 17.00 LFCS Seminar: Tuesday 11 March: Willem Heijltjes Willem Heijltjes, University of Bath https://people.bath.ac.uk/wbh22/ G.03
LFCS Seminar: Tuesday 11 March: Willem Heijltjes Speaker: Willem Heijltjes Title: The Functional Machine Calculus Abstract: The Functional Machine Calculus (FMC) is a new approach to combining the lambda-calculus with computational effects, along similar lines as Moggi's monadic approach, Levy's call-by-push-value, and Plotkin and Pretnar's effect handlers. Its point of departure is to view the lambda-calculus as a simple instruction language for a call-by-name stack machine in the style of Krivine, where application pushes its argument and abstraction pops. The FMC then consists of three extensions. The first is to allow multiple independent stacks, which are then used to model higher-order store, input/output, and probabilistic choice (as a probabilistically generated stream). The second is to introduce imperative sequencing and skip, modelled through a standard continuation stack, which allows to encode call-by-value as well as the computational metalanguage and call-by-push-value. The third is to take imperative skip, which represents successful termination, and parameterize it to model exceptions as well. Sequencing is made conditional accordingly, and a natural notion of loop is introduced. This allows to further capture exception handling, constants, data types, and while-loops. With this approach, key features of the lambda-calculus extend to imperative programming. The abstract machine allows to derive a confluent notion of reduction, extending beta-reduction, and a notion of simple types that (in the absence of iteration) guarantees termination of the machine. Mar 11 2025 16.10 - 17.00 LFCS Seminar: Tuesday 11 March: Willem Heijltjes Willem Heijltjes, University of Bath https://people.bath.ac.uk/wbh22/ G.03
Mar 11 2025 16.10 - 17.00 LFCS Seminar: Tuesday 11 March: Willem Heijltjes Willem Heijltjes, University of Bath https://people.bath.ac.uk/wbh22/
