Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic

@misc{citeulike:401369, abstract = {this paper. This calculus satis es cut-elimination, as for instance shown (in a more complicated form) in [Wij90]. This calculus is dierent from what is usually taken as the basic constructive system K, as we do not assume the distribution of possibility (3) over disjunctions neither in its binary form 3(A \_ B) ! (3A \_ 3B) nor in its nullary form 3? ! ? The sequent calculus above corresponds to an axiomatic formulation given by axioms for intuitionistic logic, plus axioms: 2(A ! B) !...}, author = {Bellin, Gianluigi and de Paiva, Valeria and Ritter, Eike}, citeulike-article-id = {401369}, keywords = {categorical, logic, modal}, posted-at = {2005-11-19 16:57:25}, priority = {0}, title = {Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.2874} }

TY - GEN ID - citeulike:401369 L3 - citeulike-article-id:401369 N2 - this paper. This calculus satis es cut-elimination, as for instance shown (in a more complicated form) in [Wij90]. This calculus is dierent from what is usually taken as the basic constructive system K, as we do not assume the distribution of possibility (3) over disjunctions neither in its binary form 3(A _ B) ! (3A _ 3B) nor in its nullary form 3? ! ? The sequent calculus above corresponds to an axiomatic formulation given by axioms for intuitionistic logic, plus axioms: 2(A ! B) !... TI - Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic KW - categorical KW - logic KW - modal AU - Bellin, Gianluigi AU - de Paiva, Valeria AU - Ritter, Eike UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.2874 ER -