G"odel Logic: from Natural Deduction to Parallel Computation

Propositional G"odel logic extends intuitionistic logic with the non-constructive principle of linearity Arightarrow B lor Brightarrow 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.