Fibrational modal type theory

DOI10.1016/j.entcs.2016.06.010zbMath1394.03037WikidataQ56994433 ScholiaQ56994433MaRDI QIDQ1744413

Eike Ritter, V. C. V. de Paiva

Publication date: 23 April 2018

Full work available at URL: https://doi.org/10.1016/j.entcs.2016.06.010

zbMATH Keywords

modal logic; fibrations; categorical models

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03B70: Logic in computer science

03G30: Categorical logic, topoi

Related Items

Modal dependent type theory and dependent right adjoints, Modalities in homotopy type theory

Uses Software

• Automath
• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Categorical logic and type theory
• Categorical abstract machines for higher-order typed \(\lambda\)-calculi
• Propositional lax logic
• Monad as modality
• On an intuitionistic modal logic
• A judgmental reconstruction of modal logic
• Integrating Linear and Dependent Types
• A modal analysis of staged computation
• Intuitionistic tense and modal logic
• Computational types from a logical perspective
• Internal type theory
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Propositions as [Types]
• Combining proofs and programs in a dependently typed language
• Homotopy Type Theory: Univalent Foundations of Mathematics