Projects per year
Abstract
The Functional Machine Calculus (FMC), recently introduced by the authors, is a generalization of the lambdacalculus which may faithfully encode the effects of higherorder mutable store, I/O and probabilistic/nondeterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects.
In this paper, we explore the denotational semantics of the FMC. We have three main contri butions: first, we argue that its syntax – in which both effects and lambdacalculus are realised using the same syntactic constructs – is semantically natural, corresponding closely to the structure of a Scottstyle domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambdacalculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
In this paper, we explore the denotational semantics of the FMC. We have three main contri butions: first, we argue that its syntax – in which both effects and lambdacalculus are realised using the same syntactic constructs – is semantically natural, corresponding closely to the structure of a Scottstyle domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambdacalculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
Original language  English 

Number of pages  18 
Publication status  Epub ahead of print  24 Nov 2022 
Fingerprint
Dive into the research topics of 'The Functional Machine Calculus II: Semantics'. 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