Projects per year
Abstract
The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic 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 contributions: first, we argue that its syntax – in which both effects and lambda-calculus are realised using the same syntactic constructs – is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, 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 |
DOIs | |
Publication status | Published - 3 Feb 2023 |
Bibliographical note
Funding Information:Funding Willem Heijltjes: EPSRC Grant EP/R029121/1 Typed lambda-calculi with sharing and unsharing.
Publisher Copyright:
© Chris Barrett, Willem Heijltjes, and Guy McCusker.
Keywords
- computational effects
- denotational semantics
- lambda-calculus
- strong normalization
ASJC Scopus subject areas
- Software
Fingerprint
Dive into the research topics of 'The Functional Machine Calculus II: Semantics'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Typed Lambda-Calculi with Sharing and Unsharing
Heijltjes, W. (PI)
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council