Image de couverture de livre

Eliminating reversals from cubical type theories

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Cavallo, Evan, Sattler, Christian
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

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

Univalence without function extensionality
par: Cavallo, Evan, et autres
Publié: (2026)

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

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

Constructive higher sheaf models with applications to synthetic mathematics
par: Coquand, Thierry, et autres
Publié: (2026)

Automating Boundary Filling in Cubical Type Theories
par: Doré, Maximilian, et autres
Publié: (2024)

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

Natural numbers from integers
par: Sattler, Christian, et autres
Publié: (2024)

On the Cut Elimination of Weak Intuitionistic Tense Logic
par: Wang, Yiheng, et autres
Publié: (2024)

Internalizing Representation Independence with Univalence
par: Angiuli, Carlo, et autres
Publié: (2020)

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

Degrees of incomputability, realizability and constructive reverse mathematics
par: Kihara, Takayuki
Publié: (2020)

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

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

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

Cut-Elimination for the Bimodal Logic GR
par: Kushida, Hirohiko
Publié: (2026)

Goedel Logics: On the Elimination of The Absoluteness Operator
par: Baaz, Matthias, et autres
Publié: (2026)

SAT-Inspired Higher-Order Eliminations
par: Blanchette, Jasmin, et autres
Publié: (2022)

On Efficient Algorithms For Partial Quantifier Elimination
par: Goldberg, Eugene
Publié: (2024)

IMELL Cut Elimination with Linear Overhead
par: Accattoli, Beniamino, et autres
Publié: (2024)

Partial Quantifier Elimination By Certificate Clauses
par: Goldberg, Eugene
Publié: (2020)

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)

On Symbol Elimination and Uniform Interpolation in Theory Extensions
par: Sofronie-Stokkermans, Viorica
Publié: (2025)

Structure-Aware Computing, Partial Quantifier Elimination And SAT
par: Goldberg, Eugene
Publié: (2024)

The Proof-Theoretic Origin of Double Negation Introduction & Elimination
par: Irani, Khashayar
Publié: (2025)

Variable Elimination as Rewriting in a Linear Lambda Calculus
par: Ehrhard, Thomas, et autres
Publié: (2025)

Integer Linear-Exponential Programming in NP by Quantifier Elimination
par: Chistikov, Dmitry, et autres
Publié: (2024)

Pseudo-Complex Quantifier Elimination
par: Faroß, Nicolas, et autres
Publié: (2026)

Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic
par: Acclavio, Matteo, et autres
Publié: (2023)

A Semantic Proof of Generalised Cut Elimination for Deep Inference
par: Atkey, Robert, et autres
Publié: (2024)

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

Large Language Model for OWL Proofs
par: Yang, Hui, et autres
Publié: (2026)

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

Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
par: Curzi, Gianluca, et autres
Publié: (2026)

Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
par: Maniwa, Akinori, et autres
Publié: (2024)

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
par: Amat, Nicolas, et autres
Publié: (2024)

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