Classical natural deduction for S4 modal logic

DOI10.1007/s00354-010-0099-3zbMath1251.68071OpenAlexW2067687795MaRDI QIDQ1758660

Daisuke Kimura, Yoshihiko Kakutani

Publication date: 16 November 2012

Published in: New Generation Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00354-010-0099-3

zbMATH Keywords

functional programmingCurry-Howard isomorphismlambda-calculusclassical S4 modal logicstaged computation

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Related Items

Unnamed Item

Uses Software

• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MiniML
• MetaML and multi-stage programming with explicit annotations
• On an intuitionistic modal logic
• On theories with a combinatorial definition of 'equivalence'
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• A judgmental reconstruction of modal logic
• The duality of computation
• A modal analysis of staged computation
• A new S4 classical modal logic in natural deduction
• Call-by-Name and Call-by-Value in Normal Modal Logic
• An environment machine for the λμ-calculus
• Term Rewriting and Applications