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 language | English |
---|---|
Title of host publication | LICS ’18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science |
Publisher | Association for Computing Machinery |
Pages | 839-848 |
Number of pages | 10 |
ISBN (Print) | 9781450355834 |
DOIs | |
Publication status | Published - 9 Jul 2018 |
Fingerprint
Dive into the research topics of 'A functional interpretation with state'. Together they form a unique fingerprint.Profiles
-
Thomas Powell
- Department of Computer Science - Senior Lecturer
- Mathematical Foundations of Computation
Person: Research & Teaching