The Functional Machine Calculus

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

55 Downloads (Pure)


This paper presents the Functional Machine Calculus (FMC) as a simple model of higher-order computation with "reader/writer" effects: higher-order mutable store, input/output, and probabilistic and non-deterministic computation. The FMC derives from the lambda-calculus by taking the standard operational perspective of a call-by-name stack machine as primary, and introducing two natural generalizations. One, "locations", introduces multiple stacks, which each may represent an effect and so enable effect operators to be encoded into the abstraction and application constructs of the calculus. The second, "sequencing", is known from kappa-calculus and concatenative programming languages, and introduces the imperative notions of "skip" and "sequence". This enables the encoding of reduction strategies, including call-by-value lambda-calculus and monadic constructs. The encoding of effects into generalized abstraction and application means that standard results from the lambda-calculus may carry over to effects. The main result is confluence, which is possible because encoded effects reduce algebraically rather than operationally. Reduction generates the familiar algebraic laws for state, and unlike in the monadic setting, reader/writer effects combine seamlessly. A system of simple types confers termination of the machine.
Original languageEnglish
Title of host publicationProceedings of MFPS XXXVIII
Number of pages24
Publication statusPublished - 22 Feb 2023
Event38th International Conference on Mathematical Foundations of Programming Semantics - Cornell University, Ithaca, USA United States
Duration: 11 Jul 202213 Jul 2022

Publication series

NameElectronic Notes in Theoretical Informatics and Computer Science
ISSN (Electronic)2969-2431


Conference38th International Conference on Mathematical Foundations of Programming Semantics
Abbreviated titleMFPS 2022
Country/TerritoryUSA United States

Bibliographical note

work was supported by EPSRC Project EP/R029121/1


Dive into the research topics of 'The Functional Machine Calculus'. Together they form a unique fingerprint.

Cite this