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 

Title of host publication  Proceedings of MFPS XXXVIII 
Publisher  Episciences 
Chapter  6 
Number of pages  24 
Volume  1 
Edition  2023 
DOIs  
Publication status  Published  22 Feb 2023 
Event  38th International Conference on Mathematical Foundations of Programming Semantics  Cornell University, Ithaca, USA United States Duration: 11 Jul 2022 → 13 Jul 2022 
Publication series
Name  Electronic Notes in Theoretical Informatics and Computer Science 

ISSN (Electronic)  29692431 
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 
Projects
 1 Finished

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