并行程序的经典证明
Classical Proofs as Parallel Programs
摘要：
我们介绍了经典逻辑的第一个证明作为并行程序的对应。我们定义了一个并行的和更强大的扩展的简单类型的λ演算对应的分析自然演绎的基础上排中律。由此产生的函数式语言具有进程之间的自然高阶通信机制，也支持广播。规范化过程使用了实现处理和传输进程闭包的新技术的归约。
英文摘要：
We introduce a first proofs-as-parallel-programs correspondence for classical logic. We define a parallel and more powerful extension of the simply typed lambda calculus corresponding to an analytic natural deduction based on the excluded middle law. The resulting functional language features a natural higher-order communication mechanism between processes, which also supports broadcasting. The normalization procedure makes use of reductions that implement novel techniques for handling and transmitting process closures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
