Fibrational modal type theory
From MaRDI portal
Publication:1744413
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
03B45: Modal logic (including the logic of norms)
03B70: Logic in computer science
03G30: Categorical logic, topoi
Related Items
Unnamed Item, Modal dependent type theory and dependent right adjoints, Modalities in homotopy type theory, Modality via iterated enrichment
Uses Software
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item