Classical natural deduction for S4 modal logic
From MaRDI portal
Publication:1758660
DOI10.1007/s00354-010-0099-3zbMath1251.68071MaRDI 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
functional programming; Curry-Howard isomorphism; lambda-calculus; classical S4 modal logic; staged computation
03B45: Modal logic (including the logic of norms)
68N18: Functional programming and lambda calculus
03B70: Logic in computer science
Related Items
Uses Software
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