Extended Addressing Machines for PCF, with Explicit SubstitutionsArticle
Authors: Benedetto Intrigila ; Giulio Manzonetto ; Nicolas Munnich
NULL##NULL##NULL
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.
Comment: 16 pages, 5 pages appendix
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- Probabilistic program semantics; Funder: French National Research Agency (ANR); Code: ANR-19-CE48-0014
- Combining Graded and Intersection Types for the Analyses of Resources; Funder: French National Research Agency (ANR); Code: ANR-18-CE25-0001