一句话：提出带全局状态的 Gödel 函数解释，用状态有效性处理 contraction，并改进证明抽取程序的效率与语义理解。
该文研究 Gödel 函数解释中证明抽取程序的计算内容与 contraction 问题。传统解释抽取的是系统 T 的纯项，难以直接携带关于数学环境的信息。作者提出一种带全局状态的函数解释：抽取程序不再只是纯项，而是与状态交互，状态用于存储底层数学环境的相关信息；程序的有效性可依赖状态的有效性，从而为处理 contraction 问题提供新途径。该表述还给出对证明计算内容的清晰语义洞察，并提供提升抽取程序效率的方法。摘要未报告实现或实验评估，工作以理论构造和语义分析为主。
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.
DOI 原文 ·
@inproceedings{paperbot4310,
title = {A functional interpretation with state},
author = {Thomas Powell},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209134}
}