The significance of the extended Curry Howard correspondence relating the simply typed lambda calculus to proofs of intuitionistic propositioinal logic and to appropriate classes of categories are widely known. In this note we pursue an analogous correspondence for a basic intuitionistic modal logic IK with both the necessity and the possibility operators.
Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic
BELLIN, Gianluigi;
2001-01-01
Abstract
The significance of the extended Curry Howard correspondence relating the simply typed lambda calculus to proofs of intuitionistic propositioinal logic and to appropriate classes of categories are widely known. In this note we pursue an analogous correspondence for a basic intuitionistic modal logic IK with both the necessity and the possibility operators.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
