A functional interpretation with state

Thomas Powell

doi:10.1145/3209108.3209134

A functional interpretation with state

Technische Universität Darmstadt

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

6 Citations (SciVal)

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	https://doi.org/10.1145/3209108.3209134
Publication status	Published - 9 Jul 2018

Access to Document

10.1145/3209108.3209134

https://dl.acm.org/doi/10.1145/3209108.3209134

Thomas Powell
- trjp20bath.acuk
- Department of Computer Science - Senior Lecturer
- Mathematical Foundations of Computation
Person: Research & Teaching

Cite this

@inproceedings{8805c0cce3ed4a4989eb10c7a60db925,

title = "A functional interpretation with state",

abstract = "We present a new variant of G{\"o}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.",

author = "Thomas Powell",

year = "2018",

month = jul,

day = "9",

doi = "10.1145/3209108.3209134",

language = "English",

isbn = "9781450355834",

pages = "839--848",

booktitle = "LICS {\textquoteright}18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science",

publisher = "Association for Computing Machinery",

address = "USA United States",

}

TY - GEN

T1 - A functional interpretation with state

AU - Powell, Thomas

PY - 2018/7/9

Y1 - 2018/7/9

N2 - 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.

AB - 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.

U2 - 10.1145/3209108.3209134

DO - 10.1145/3209108.3209134

M3 - Chapter in a published conference proceeding

SN - 9781450355834

SP - 839

EP - 848

BT - LICS ’18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

PB - Association for Computing Machinery

ER -

A functional interpretation with state

Abstract

Access to Document

Fingerprint

Profiles

Thomas Powell

Cite this