Extended addressing machines (EAMs) have been introduced to represent higher-order sequential computations. Previously, we have shown that they are capable of simulating -- via an easy encoding -- the operational semantics of PCF, extended with explicit substitutions. In this paper we prove that the simulation is actually an equivalence: a PCF program terminates in a numeral exactly when the corresponding EAM terminates in the same numeral. It follows that the model of PCF obtained by quotienting typable EAMs by a suitable logical relation is adequate. From a definability result stating that every EAM in the model can be transformed into a PCF program with the same observational behavior, we conclude that the model is fully abstract for PCF.arXiv admin note: text overlap with arXiv:2212.11147

@article{paperbot3385,
  title = {A Fully Abstract Model of PCF Based on Extended Addressing Machines},
  author = {Benedetto Intrigila and Giulio Manzonetto and Nicolas Munnich},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 3},
  year = {2025},
  doi = {10.46298/lmcs-21(3:17)2025}
}