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

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.
intuitionistic modal logic; Curry Howard isomorphism; Categorical logic
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/110
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact