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.
|Title of host publication||LICS ’18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science|
|Publisher||Association for Computing Machinery|
|Number of pages||10|
|Publication status||Published - 9 Jul 2018|