Willem Heijltjes - The Functional Machine Calculus III: Control

entics:16682 - Electronic Notes in Theoretical Informatics and Computer Science, December 20, 2025, Volume 5 - Proceedings of MFPS XLI - https://doi.org/10.46298/entics.16682
The Functional Machine Calculus III: ControlArticle

Authors: Willem Heijltjes

    The Functional Machine Calculus (Heijltjes 2022) is a new approach to unifying the imperative and functional programming paradigms. It extends the lambda-calculus, preserving the key features of confluent reduction and typed termination, to embed computational effects, evaluation strategies, and control flow operations. The first instalment modelled sequential higher-order computation with global store, input/output, probabilities, and non-determinism, and embedded both the call-by-name and call-by-value lambda-calculus, as well as Moggi's computational metalanguage and Levy's call-by-push-value. The present paper extends the calculus from sequential to branching and looping control flow. This allows the faithful embedding of a minimal but complete imperative language, including conditionals, exception handling, and iteration, as well as constants and algebraic data types.
    The calculus is defined through a simple operational semantics, extending the (simplified) Krivine machine for the lambda-calculus with multiple operand stacks to model effects and a continuation stack to model sequential, branching, and looping computation. It features a confluent reduction relation and a system of simple types that guarantees termination of the machine and strong normalization of reduction (in the absence of iteration). These properties carry over to the embedded imperative language, providing a unified functional-imperative model of computation that supports simple types, a direct and intuitive operational semantics, and a confluent reduction semantics.


    Volume: Volume 5 - Proceedings of MFPS XLI
    Published on: December 20, 2025
    Accepted on: October 15, 2025
    Submitted on: April 3, 2025
    Keywords: Programming Languages, Logic in Computer Science

    Consultation statistics

    This page has been seen 37 times.
    This article's PDF has been downloaded 15 times.