Godel Logic: from Natural Deduction to Parallel Computation

Propositional Godel logic G extends intuitionistic logic with the non-constructive principle of linearity (A -> B) V (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 lambda-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.