scientific article; zbMATH DE number 1231474

MaRDI QIDQ4222777zbMATH OpenFDO

Authors 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

zbMATH Keywords

intuitionistic linear logicintuitionistic modal logic S4proof term calculustype checking algorithm

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1508934
• A modal analysis of staged computation
• Fitch-style modal lambda calculi
• scientific article; zbMATH DE number 1420785
• scientific article; zbMATH DE number 2209442

Cited in

(23)

• Light types for polynomial time computation in lambda calculus
• On the geometry of intuitionistic S4 proofs
• Safe recursion with higher types and BCK-algebra
• Fitch-style modal lambda calculi
• Classical natural deduction for S4 modal logic
• Denotation of contextual modal type theory (CMTT): syntax and meta-programming
• Connectionist computations of intuitionistic reasoning
• Path calculus in the modal logic S4
• A modal analysis of staged computation
• Loop-free calculus for modal logic S4. II
• scientific article; zbMATH DE number 1223735 (Why is no real title available?)
• A modal view of linear logic
• scientific article; zbMATH DE number 1508934 (Why is no real title available?)
• scientific article; zbMATH DE number 2174387 (Why is no real title available?)
• scientific article; zbMATH DE number 1418450 (Why is no real title available?)
• scientific article; zbMATH DE number 1420785 (Why is no real title available?)
• A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4
• The basic intuitionistic logic of proofs
• scientific article; zbMATH DE number 2209442 (Why is no real title available?)
• Primitive recursion for higher-order abstract syntax
• Normalization by evaluation for modal dependent type theory
• Realising intensional S4 and GL modalities
• Cut-free Gentzen calculus for multimodal CK

Describes a project that uses

Uses Software

• Elf

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4222777)