一句话：为命题 Gödel 逻辑 G 建立 Curry–Howard 对应，用自然演绎类型系统刻画带同步通信的并行函数式计算。
命题 Gödel 逻辑 G 在直觉主义逻辑上加入了非构造性的线性公理 (A → B) ∨ (B → A)，但其计算解释长期缺失。本文为 G 引入 Curry–Howard 对应，证明一个简单的自然演绎演算可作为类型系统，由此得到一种扩展简单类型 λ-演算的函数式语言：它通过并行进程之间的同步通信机制进行计算，并因此比简单类型 λ-演算具有更强表达力。论文还给出规范化证明，其终止性论证和证明变换体现了代码移动等机制。该结果给出了 G 的计算解释，从而证明了 A. Avron 于 1991 年提出的论题。
Propositional Gödel logic G extends intuitionistic logic with the non-constructive principle of linearity (A → B) ∨ (B → A). We introduce a Curry-Howard correspondence for G and show that a simple natural deduction calculus can be used as a typing system. The resulting functional language extends the simply typed λ-calculus via a synchronous communication mechanism between parallel processes, which increases its expressive power. The normalization proof employs original termination arguments and proof transformations implementing forms of code mobility. Our results provide a computational interpretation of G, thus proving A. Avron's 1991 thesis.