License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.10
URN: urn:nbn:de:0030-drops-174716
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17471/
Go to the corresponding LIPIcs Volume Portal

Barrett, Chris ; Heijltjes, Willem ; McCusker, Guy

The Functional Machine Calculus II: Semantics

pdf-format:
LIPIcs-CSL-2023-10.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{barrett_et_al:LIPIcs.CSL.2023.10,
  author =	{Barrett, Chris and Heijltjes, Willem and McCusker, Guy},
  title =	{{The Functional Machine Calculus II: Semantics}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17471},
  URN =		{urn:nbn:de:0030-drops-174716},
  doi =		{10.4230/LIPIcs.CSL.2023.10},
  annote =	{Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization}
}

Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization
Collection: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Issue Date: 2023
Date of publication: 01.02.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI