Benedetto Intrigila ; Giulio Manzonetto ; Nicolas Munnich - Extended Addressing Machines for PCF, with Explicit Substitutions

entics:10533 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII - https://doi.org/10.46298/entics.10533
Extended Addressing Machines for PCF, with Explicit SubstitutionsArticle

Authors: Benedetto Intrigila ; Giulio Manzonetto ; Nicolas Munnich

    Addressing machines have been introduced as a formalism to construct models of the pure, untyped lambda-calculus. We extend the syntax of their programs by adding instructions for executing arithmetic operations on natural numbers, and introduce a reflection principle allowing certain machines to access their own address and perform recursive calls. We prove that the resulting extended addressing machines naturally model a weak call-by-name PCF with explicit substitutions. Finally, we show that they are also well-suited for representing regular PCF programs (closed terms) computing natural numbers.


    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: December 22, 2022
    Submitted on: December 22, 2022
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Combining Graded and Intersection Types for the Analyses of Resources; Funder: French National Research Agency (ANR); Code: ANR-18-CE25-0001
    • Probabilistic program semantics; Funder: French National Research Agency (ANR); Code: ANR-19-CE48-0014

    Consultation statistics

    This page has been seen 88 times.
    This article's PDF has been downloaded 77 times.