Modal type theory based on the intuitionistic modal logic IEL^-

DOI10.1007/978-3-030-36755-8_15MaRDI QIDQ2177591zbMATH OpenOpenAlexFDO

Authors Daniel Rogozin

Publication date 6 May 2020

Full work available at URL https://doi.org/10.1007/978-3-030-36755-8_15

zbMATH Keywords

applicative functorfunctional programmingintuitionistic epistemic logicmodal type theory

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18)

Recommendations

• Categorical and algebraic aspects of the intuitionistic modal logic \(\mathrm{IEL}^{\text{--}}\) and its predicate extensions
• Intuitionistic epistemology and modal logics of verification
• Sequent Calculus for Intuitionistic Epistemic Logic IEL
• Modal pure type systems. Type theory for knowledge representation
• Cut elimination and complexity bounds for intuitionistic epistemic logic

Cited in

(6)

• Modal pure type systems. Type theory for knowledge representation
• Curry-Howard-Lambek correspondence for intuitionistic belief
• Intuitionistic modal logic: a 15-year retrospective
• Categorical and algebraic aspects of the intuitionistic modal logic \(\mathrm{IEL}^{\text{--}}\) and its predicate extensions
• scientific article; zbMATH DE number 7599983 (Why is no real title available?)
• Linear depth deduction with subformula property for intuitionistic epistemic logic

This page was built for publication: Modal type theory based on the intuitionistic modal logic \(\mathrm{IEL}^{-}\)

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