Image de couverture de livre

Unifying cubical and multimodal type theory

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Aagaard, Frederik Lerbjerg, Kristensen, Magnus Baunsgaard, Gratzer, Daniel, Birkedal, Lars
Format:	Preprint
Publié:	2022
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

A denotationally-based program logic for higher-order store
par: Aagaard, Frederik Lerbjerg, et autres
Publié: (2023)

Normalization for multimodal type theory
par: Gratzer, Daniel
Publié: (2023)

Controlling unfolding in type theory
par: Gratzer, Daniel, et autres
Publié: (2022)

The $\infty$-category of $\infty$-categories in simplicial type theory
par: Gratzer, Daniel, et autres
Publié: (2026)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
par: Gratzer, Daniel, et autres
Publié: (2024)

Strict universes for Grothendieck topoi
par: Gratzer, Daniel, et autres
Publié: (2022)

Eliminating reversals from cubical type theories
par: Cavallo, Evan, et autres
Publié: (2026)

Yet another cubical type theory, but via a semantic approach
par: Kapulkin, Chris, et autres
Publié: (2025)

Normal forms in cubical type theory
par: Huang, Xu
Publié: (2026)

Semantics of multimodal adjoint type theory
par: Shulman, Michael
Publié: (2023)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
par: Li, Kwing Hei, et autres
Publié: (2025)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
par: de Medeiros, Markus, et autres
Publié: (2026)

Reasoning about Weak Isolation Levels in Separation Logic
par: Mathiasen, Anders Alnor, et autres
Publié: (2025)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
par: de Jong, Tom, et autres
Publié: (2026)

Almost-Sure Termination by Guarded Refinement
par: Gregersen, Simon Oddershede, et autres
Publié: (2024)

Generic bidirectional typing for dependent type theories
par: Felicissimo, Thiago
Publié: (2023)

The equivariant model structure on cartesian cubical sets
par: Awodey, Steve, et autres
Publié: (2024)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
par: Li, Kwing Hei, et autres
Publié: (2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
par: Haselwarter, Philipp G., et autres
Publié: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
par: Haselwarter, Philipp G., et autres
Publié: (2026)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
par: Timany, Amin, et autres
Publié: (2021)

Homotopy type theory as a language for diagrams of $\infty$-logoses
par: Uemura, Taichi
Publié: (2022)

Formalizing two-level type theory with cofibrant exo-nat
par: Uskuplu, Elif
Publié: (2023)

Directed type theory, with a twist
par: Rivera, Fernando Rafael Chu, et autres
Publié: (2026)

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
par: Spadetto, Matteo
Publié: (2023)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
par: Aguirre, Alejandro, et autres
Publié: (2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
par: Haselwarter, Philipp G., et autres
Publié: (2024)

The Yoneda embedding in simplicial type theory
par: Gratzer, Daniel, et autres
Publié: (2025)

Compositional pre-processing for automated reasoning in dependent type theory
par: Blot, Valentin, et autres
Publié: (2022)

Directed univalence in simplicial homotopy type theory
par: Gratzer, Daniel, et autres
Publié: (2024)

Bringing closure to theory combination properties
par: Toledo, Guilherme V., et autres
Publié: (2026)

Undecidability of theories of semirings with fixed points
par: Das, Anupam, et autres
Publié: (2025)

Strong negation in the theory of computable functionals TCF
par: Köpp, Nils, et autres
Publié: (2022)

On proving consistency of equational theories in Bounded Arithmetic
par: Beckmann, Arnold, et autres
Publié: (2022)

Classifying covering types in homotopy type theory
par: Mimram, Samuel, et autres
Publié: (2025)

Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
par: Lyon, Tim S.
Publié: (2024)

Being polite is not enough (and other limits of theory combination)
par: Toledo, Guilherme V., et autres
Publié: (2025)

Central H-spaces and banded types
par: Buchholtz, Ulrik, et autres
Publié: (2023)

The proof theory and semantics of second-order (intuitionistic) tense logic
par: Becker, Justus, et autres
Publié: (2026)

Bijective proofs for Eulerian numbers of types B and D
par: Santocanale, Luigi
Publié: (2021)