ICFP 2021
Sun 22 - Sat 28 August 2021
Sun 22 Aug 2021 18:00 - 18:30 at HOPE - Session 2

This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with effects, including mutable store, input and output, and probabilistic and non-deterministic computation as special cases of input. The FMC is derived from the lambda-calculus via two independent generalizations. One enables the encoding of effects into the calculus; the other provides control when they are executed, and encodes the imperative features of “sequencing” and “skip”.

These generalizations are particularly natural from the perspective of the FMC as an instruction language for a simple stack machine (a simplified Krivine Abstract Machine, and the “M” in “FMC”). The first generalization corresponds to allowing multiple stacks, which may represent storage cells and input and output streams to capture the operational semantics of effects. The second generalization gives composition of instruction sequences, and the empty sequence as a unit.

The FMC naturally encodes various previous approaches, including Plotkin’s Call-By-Value lambda-calculus, Moggi’s Computational Metalanguage, and Levy’s Call-By-Push-Value. The calculus is confluent, which is possible because beta-reduction encodes the evaluation of effects via their algebraic equations, not their operational semantics. Different evaluation strategies in the lambda-calculus are captured by different encodings into the FMC.

The FMC can be simply typed, and a simple, direct proof shows that types confer termination of the stack machine, or equivalently of weak head reduction. Types give a natural solution to the problem of types for higher-order store.

Sun 22 Aug

Displayed time zone: Seoul change

18:00 - 19:30
Session 2HOPE at HOPE
18:00
30m
Talk
The Functional Machine Calculus
HOPE
Willem Heijltjes University of Bath
18:30
30m
Talk
Formalising Algebraic Effects with Non-Recoverable Failure
HOPE
Timotej Tomandl University of Kent, Dominic Orchard University of Kent, UK
Pre-print
19:00
30m
Talk
Computational calculus: bridging reduction and evaluation
HOPE
Claudia Faggian Université de Paris & CNRS, Giulio Guerrieri University of Bath, Riccardo Treglia Università di Torino
File Attached