Multimodal dependent type theory
From MaRDI portal
Recommendations
Cites work
- A contextual logical framework
- A Generalized Modality for Recursion
- A judgmental reconstruction of modal logic
- A model of guarded recursion with clock synchronisation
- A presheaf model of parametric type theory
- A type theory for productive coprogramming via guarded recursion
- Adjoint logic with a 2-category of modes
- An algorithm for type-checking dependent types
- Applicative programming with effects
- Axiomatic cohesion
- Brouwer's fixed-point theorem in real-cohesive homotopy type theory
- Canonicity and normalization for dependent type theory
- Categorical homotopy theory
- Category theory in context
- Contextual modal type theory
- Degrees of relatedness. A unified framework for parametricity, irrelevance, ad hoc polymorphism, intersections, unions and algebra in dependent type theory
- First steps in synthetic guarded domain theory: step-indexing in the topos of trees
- Fitch-style modal lambda calculi
- Generalized algebraic theories and contextual categories
- Guard your daggers and traces: on the equational properties of guarded (co-)recursion
- Homotopy type theory. Univalent foundations of mathematics
- scientific article; zbMATH DE number 4177054 (Why is no real title available?)
- scientific article; zbMATH DE number 5761737 (Why is no real title available?)
- scientific article; zbMATH DE number 3950781 (Why is no real title available?)
- scientific article; zbMATH DE number 1241699 (Why is no real title available?)
- scientific article; zbMATH DE number 1302063 (Why is no real title available?)
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- scientific article; zbMATH DE number 7204444 (Why is no real title available?)
- scientific article; zbMATH DE number 7297837 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3367095 (Why is no real title available?)
- Internal type theory
- Internal universes in models of homotopy type theory
- Logic Programming with Focusing Proofs in Linear Logic
- Modalities in homotopy type theory
- Natural models of homotopy type theory
- Normalisation by evaluation for dependent types
- Notions of computation and monads
- On an intuitionistic modal logic
- On irrelevance and algorithmic equality in predicative type theory
- On the unity of logic
- Pointers in Recursion: Exploring the Tropics
- Polarised subtyping for sized types
- Productive coprogramming with guarded recursion
- Programming and reasoning with guarded recursion for coinductive types
- Quantum gauge field theory in cohesive homotopy type theory
- Sheaves in geometry and logic: a first introduction to topos theory
- The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
- The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
- The clocks they are adjunctions. Denotational semantics for clocked type theory
- Treatise on intuitionistic type theory
- Univalence for inverse diagrams and homotopy canonicity
Cited in
(26)- Fibrational modal type theory
- Graded modal dependent type theory
- Multimodal dependent type theory
- Modal dependent type theory and dependent right adjoints
- Finitary type theories with and without contexts
- scientific article; zbMATH DE number 7779294 (Why is no real title available?)
- When programs have to watch paint dry
- Strange new universes: Proof assistants and synthetic foundations
- A general framework for the semantics of type theory
- UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
- Contextual modal type theory with polymorphic contexts
- Constructing unprejudiced extensional type theories with choices via modalities
- Transpension: the right adjoint to the Pi-type
- Normalization for multimodal type theory
- Two-dimensional Kripke semantics. II: Stability and completeness
- Semantics of multimodal adjoint type theory
- A categorical normalization proof for the modal lambda-calculus
- Normalization for multimodal type theory
- Homotopy type theory as a language for diagrams of -logoses
- A sound and complete substitution algorithm for multimode type theory
- Two-dimensional Kripke semantics i: presheaves
- Displayed type theory and semi-simplicial types
- Exponentiable functors between synthetic -categories
- ``Upon this quote I will build my Church thesis
- Primitive recursive dependent type theory
- Unifying cubical and multimodal type theory
This page was built for publication: Multimodal dependent type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5155672)
