Projects per year
Abstract
This paper presents the Functional Machine Calculus (FMC) as a simple model of higherorder computation with "reader/writer" effects: higherorder mutable store, input/output, and probabilistic and nondeterministic computation. The FMC derives from the lambdacalculus by taking the standard operational perspective of a callbyname 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 kappacalculus and concatenative programming languages, and introduces the imperative notions of "skip" and "sequence". This enables the encoding of reduction strategies, including callbyvalue lambdacalculus and monadic constructs. The encoding of effects into generalized abstraction and application means that standard results from the lambdacalculus 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 language  English 

Number of pages  24 
Publication status  Acceptance date  20 Dec 2022 
Event  38th International Conference on Mathematical Foundations of Programming Semantics  Cornell University, Ithaca, USA United States Duration: 11 Jul 2022 → 13 Jul 2022 
Conference
Conference  38th International Conference on Mathematical Foundations of Programming Semantics 

Abbreviated title  MFPS 2022 
Country/Territory  USA United States 
City  Ithaca 
Period  11/07/22 → 13/07/22 
Bibliographical note
work was supported by EPSRC Project EP/R029121/1Fingerprint
Dive into the research topics of 'The Functional Machine Calculus'. Together they form a unique fingerprint.Projects
 1 Finished

Typed LambdaCalculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council