A functional interpretation with state

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

6 Citations (SciVal)


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
Number of pages10
ISBN (Print)9781450355834
Publication statusPublished - 9 Jul 2018


Dive into the research topics of 'A functional interpretation with state'. Together they form a unique fingerprint.

Cite this