A functional interpretation with state

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

We present a new variant of Gödel's functional interpretation in which extracted programs, rather than being pure terms of system T, interact with a global state. The purpose of the state is to store relevant information about the underlying mathematical environment. Because the validity of extracted programs can depend on the validity of the state, this offers us an alternative way of dealing with the contraction problem. Furthermore, this new formulation of the functional interpretation gives us a clear semantic insight into the computational content of proofs, and provides us with a way of improving the efficiency of extracted programs.
Original languageEnglish
Title of host publicationLICS ’18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherAssociation for Computing Machinery
Pages839-848
ISBN (Print)9781450355834
DOIs
Publication statusPublished - 2018

Profiles

No photo of Thomas Powell

Cite this

Powell, T. (2018). A functional interpretation with state. In LICS ’18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 839-848). Association for Computing Machinery. https://doi.org/10.1145/3209108.3209134