Image de couverture de livre

Directed type theory, with a twist

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Rivera, Fernando Rafael Chu, North, Paige Randall
Format:	Preprint
Publié:	2026
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

Functoriality of Enriched Data Types
par: Mulder, Lukas, et autres
Publié: (2025)

Univalent Double Categories
par: van der Weide, Niels, et autres
Publié: (2023)

From Semantics to Syntax: A Type Theory for Comprehension Categories
par: Najmaei, Niyousha, et autres
Publié: (2025)

Measuring data types
par: Mulder, Lukas, et autres
Publié: (2024)

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

Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$
par: de Jong, Tom
Publié: (2024)

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

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

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

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

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

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

Unifying cubical and multimodal type theory
par: Aagaard, Frederik Lerbjerg, et autres
Publié: (2022)

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

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

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

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)

A concrete model for a typed linear algebraic lambda calculus
par: Díaz-Caro, Alejandro, et autres
Publié: (2018)

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)

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

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)

Extracting efficient exact real number computation from proofs in constructive type theory
par: Konečný, Michal, et autres
Publié: (2022)

Wider systems for linear logic with fixed points: proof theory and complexity
par: Das, Anupam, et autres
Publié: (2026)

List types for resource aware languages: an implicit name approach
par: Ghilezan, Silvia, et autres
Publié: (2021)

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

A proof theory of (omega-)context-free languages, via non-wellfounded proofs
par: Das, Anupam, et autres
Publié: (2024)

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

Hypercubical manifolds in homotopy type theory
par: Mimram, Samuel, et autres
Publié: (2025)

Basis-Sensitive Quantum Typing via Realisability
par: Díaz-Caro, Alejandro, et autres
Publié: (2025)

Monoidal weak omega-categories as models of a type theory
par: Benjamin, Thibaut
Publié: (2021)

Globular weak $ω$-categories as models of a type theory
par: Benjamin, Thibaut, et autres
Publié: (2021)

Delooping presented groups in homotopy type theory
par: Champin, Camil, et autres
Publié: (2024)

A type theory for invertibility in weak $ω$-categories
par: Benjamin, Thibaut, et autres
Publié: (2026)

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

Formalization of dependent type theory: The example of CaTT
par: Benjamin, Thibaut
Publié: (2021)

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