Laboratoire d'informatique de l'École polytechnique

Talk by Willem Heijltjes: « The Functional Machine Calculus »

Speaker: Willem Heijltjes
Location: BBB
Date: Mon, 23 May 2022, 14:00-15:00

For the next Proofs & Algorithms seminar on Monday 23rd of May at 14h00, we, at PARTOUT, are very happy to welcome Willem Heijltjes from University of Bath.

Link to the online conference

Abstract: I will present the Functional Machine Calculus (FMC), a simple model of higher-order computation with “reader/writer” effects: state, input/output, probabilities, and non-determinism. The main result is to extend two fundamental properties of the lambda-calculus to these effects: reduction in the FMC is confluent, and a system of simple types confers strong normalization.

The premise is to view the lambda-calculus as an instruction language for a simple stack machine, in the standard way of the Krivine machine, where application is “push” and abstraction is “pop”. The FMC then consists of two independent generalizations, that are natural from the perspective of the machine.

The first generalization, “locations”, is to allow multiple stacks (or streams) on the machine, each indicated by a “location”. Application and abstraction are parameterized in these locations, to give push and pop actions on the relevant stack. Then input streams, output streams, and memory cells are straightforwardly modelled by distinct locations.

The second generalization, “sequencing”, introduces sequential composition, following the perspective of terms as sequences of machine instructions, as well as a unit, the empty sequence. This is known from Hasegawa’s kappa- calculus and from concatenative programming languages, and enables the encoding of reduction strategies, including call-by-value lambda-calculus, and for the given effects, Moggi’s metalanguage, Levy’s call-by-push-value, and Haskell Arrows.

Reduction in the FMC is confluent, which is possible because encoded effect operations reduce algebraically, rather than operationally. It can be simply typed to confer strong normalization, and because effectful operations are fully typed, it has a semantics as a Cartesian closed category. Unlike in the monadic setting, reader/writer effects in the FMC combine seemlessly.


The list of next seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics