Curry-Howard Correspondence for G\"odel Logic: from Natural Deduction to Parallel Computation

Cited by: 0|Bibtex|Views0|Links

Abstract:

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 enric...More

Code:

Data:

Your rating :
0

 

Tags
Comments