scientific article; zbMATH DE number 1231474

zbMath0908.03018MaRDI QIDQ4222777

Hao Chi Wong, Frank Pfenning

Publication date: 13 December 1998

Full work available at URL: http://www.elsevier.com/cas/tree/store/tcs/free/noncas/pc/volume1.htm#pfenning

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

intuitionistic linear logicintuitionistic modal logic S4type checking algorithmproof term calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items

The basic intuitionistic logic of proofs ⋮ Normalization by evaluation for modal dependent type theory ⋮ Connectionist computations of intuitionistic reasoning ⋮ Primitive recursion for higher-order abstract syntax ⋮ Light types for polynomial time computation in lambda calculus ⋮ Cut-free Gentzen calculus for multimodal CK ⋮ Safe recursion with higher types and BCK-algebra

Uses Software

• Elf