Copertina

Eliminating reversals from cubical type theories

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Cavallo, Evan, Sattler, Christian
Natura:	Preprint
Pubblicazione:	2026
Soggetti:	Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

The equivariant model structure on cartesian cubical sets
di: Awodey, Steve, et al.
Pubblicazione: (2024)

Univalence without function extensionality
di: Cavallo, Evan, et al.
Pubblicazione: (2026)

Unifying cubical and multimodal type theory
di: Aagaard, Frederik Lerbjerg, et al.
Pubblicazione: (2022)

Yet another cubical type theory, but via a semantic approach
di: Kapulkin, Chris, et al.
Pubblicazione: (2025)

Constructive higher sheaf models with applications to synthetic mathematics
di: Coquand, Thierry, et al.
Pubblicazione: (2026)

Automating Boundary Filling in Cubical Type Theories
di: Doré, Maximilian, et al.
Pubblicazione: (2024)

Normal forms in cubical type theory
di: Huang, Xu
Pubblicazione: (2026)

Natural numbers from integers
di: Sattler, Christian, et al.
Pubblicazione: (2024)

On the Cut Elimination of Weak Intuitionistic Tense Logic
di: Wang, Yiheng, et al.
Pubblicazione: (2024)

Internalizing Representation Independence with Univalence
di: Angiuli, Carlo, et al.
Pubblicazione: (2020)

The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory
di: de Jong, Tom, et al.
Pubblicazione: (2026)

Degrees of incomputability, realizability and constructive reverse mathematics
di: Kihara, Takayuki
Pubblicazione: (2020)

Generic bidirectional typing for dependent type theories
di: Felicissimo, Thiago
Pubblicazione: (2023)

Controlling unfolding in type theory
di: Gratzer, Daniel, et al.
Pubblicazione: (2022)

Normalization for multimodal type theory
di: Gratzer, Daniel
Pubblicazione: (2023)

Cut-Elimination for the Bimodal Logic GR
di: Kushida, Hirohiko
Pubblicazione: (2026)

Goedel Logics: On the Elimination of The Absoluteness Operator
di: Baaz, Matthias, et al.
Pubblicazione: (2026)

SAT-Inspired Higher-Order Eliminations
di: Blanchette, Jasmin, et al.
Pubblicazione: (2022)

On Efficient Algorithms For Partial Quantifier Elimination
di: Goldberg, Eugene
Pubblicazione: (2024)

IMELL Cut Elimination with Linear Overhead
di: Accattoli, Beniamino, et al.
Pubblicazione: (2024)

Partial Quantifier Elimination By Certificate Clauses
di: Goldberg, Eugene
Pubblicazione: (2020)

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

Formalizing two-level type theory with cofibrant exo-nat
di: Uskuplu, Elif
Pubblicazione: (2023)

Directed type theory, with a twist
di: Rivera, Fernando Rafael Chu, et al.
Pubblicazione: (2026)

Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
di: Spadetto, Matteo
Pubblicazione: (2023)

On Symbol Elimination and Uniform Interpolation in Theory Extensions
di: Sofronie-Stokkermans, Viorica
Pubblicazione: (2025)

Structure-Aware Computing, Partial Quantifier Elimination And SAT
di: Goldberg, Eugene
Pubblicazione: (2024)

The Proof-Theoretic Origin of Double Negation Introduction & Elimination
di: Irani, Khashayar
Pubblicazione: (2025)

Variable Elimination as Rewriting in a Linear Lambda Calculus
di: Ehrhard, Thomas, et al.
Pubblicazione: (2025)

Integer Linear-Exponential Programming in NP by Quantifier Elimination
di: Chistikov, Dmitry, et al.
Pubblicazione: (2024)

Pseudo-Complex Quantifier Elimination
di: Faroß, Nicolas, et al.
Pubblicazione: (2026)

Infinitary Cut-Elimination for Non-Wellfounded Parsimonious Linear Logic
di: Acclavio, Matteo, et al.
Pubblicazione: (2023)

A Semantic Proof of Generalised Cut Elimination for Deep Inference
di: Atkey, Robert, et al.
Pubblicazione: (2024)

Compositional pre-processing for automated reasoning in dependent type theory
di: Blot, Valentin, et al.
Pubblicazione: (2022)

Large Language Model for OWL Proofs
di: Yang, Hui, et al.
Pubblicazione: (2026)

Extracting efficient exact real number computation from proofs in constructive type theory
di: Konečný, Michal, et al.
Pubblicazione: (2022)

Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm
di: Curzi, Gianluca, et al.
Pubblicazione: (2026)

Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
di: Maniwa, Akinori, et al.
Pubblicazione: (2024)

Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability
di: Amat, Nicolas, et al.
Pubblicazione: (2024)

Bringing closure to theory combination properties
di: Toledo, Guilherme V., et al.
Pubblicazione: (2026)