Curry-Howard Correspondence for G\"odel Logic: from Natural Deduction to Parallel Computation
arxiv(2016)
摘要
Propositional G\"odel logic extends intuitionistic logic with the non-constructive principle of linearity $A\rightarrow B\ \lor\ B\rightarrow A$. We introduce a Curry-Howard correspondence for this logic and show that a particularly simple natural deduction calculus can be used as a typing system. The resulting functional language enriches the simply typed lambda calculus with a synchronous communication mechanism between parallel processes. Our normalization proof employs original termination arguments and sophisticated proof transformations with a meaningful computational reading. Our results provide a computational interpretation of G\"odel logic as a logic of communicating parallel processes, thus proving Avron's 1991 conjecture.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络