Fibrational modal type theory

DOI10.1016/j.entcs.2016.06.010zbMath1394.03037OpenAlexW2472614804WikidataQ56994433 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 logicfibrationscategorical models

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Categorical logic, topoi (03G30)

Related Items (4)

Modalities in homotopy type theory ⋮ Modality via iterated enrichment ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints

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

This page was built for publication: Fibrational modal type theory