Copertina

Compositional pre-processing for automated reasoning in dependent type theory

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Blot, Valentin, Cousineau, Denis, Crance, Enzo, de Prisque, Louise Dubois, Keller, Chantal, Mahboubi, Assia, Vial, Pierre
Natura:	Preprint
Pubblicazione:	2022
Soggetti:	Logic in Computer Science
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Trocq: Proof Transfer for Free, With or Without Univalence
di: Cohen, Cyril, et al.
Pubblicazione: (2023)

Geometric theories for real number algebra without sign test or dependent choice axiom
di: Lombardi, Henri, et al.
Pubblicazione: (2024)

Théories géométriques pour l'algèbre des nombres réels sans test de signe ni axiome de choix dépendant
di: Lombardi, Henri, et al.
Pubblicazione: (2024)

Machine-Checked Categorical Diagrammatic Reasoning
di: Guillemet, Benoît, et al.
Pubblicazione: (2024)

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

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

Extensional realizability and choice for dependent types in intuitionistic set theory
di: Frittaion, Emanuele
Pubblicazione: (2024)

From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory
di: Blot, Valentin, et al.
Pubblicazione: (2024)

Multi types and reasonable space
di: Accattoli, Beniamino, et al.
Pubblicazione: (2022)

A logic for default deontic reasoning
di: Piazza, Mario, et al.
Pubblicazione: (2025)

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

Formalization of dependent type theory: The example of CaTT
di: Benjamin, Thibaut
Pubblicazione: (2021)

List types for resource aware languages: an implicit name approach
di: Ghilezan, Silvia, et al.
Pubblicazione: (2021)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
di: Ye, Kangfeng, et al.
Pubblicazione: (2023)

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)

A formal system for reasoning about assertibility, truth, and meaningfulness
di: Weaver, Nik
Pubblicazione: (2025)

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

Maximal stable quotients of invariant types in NIP theories
di: Krupiński, Krzysztof, et al.
Pubblicazione: (2023)

Model theory of differential-henselian pre-$H$-fields
di: Pynn-Coates, Nigel
Pubblicazione: (2019)

A topological counterpart of well-founded trees in dependent type theory
di: Maietti, Maria Emilia, et al.
Pubblicazione: (2023)

New foundations of reasoning via real-valued first-order logics
di: Badia, Guillermo, et al.
Pubblicazione: (2022)

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

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

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

SAT problem and Limit of Solomonoff's inductive reasoning theory
di: Pan, Feng
Pubblicazione: (2025)

The Size-Change Principle for Mixed Inductive and Coinductive types
di: Hyvernat, Pierre
Pubblicazione: (2024)

Source-level reasoning for quantitative information flow
di: Chen, Chris, et al.
Pubblicazione: (2024)

Descriptive set theory of separable Fréchet spaces
di: Braga, Bruno de Mendonça, et al.
Pubblicazione: (2025)

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

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

n-dependent continuous theories and hyperdefinable sets
di: Fernández, Adrián Portillo
Pubblicazione: (2024)

Intuitionistic modal logics: epistemic reasoning with distributed knowledge
di: Balbiani, Philippe
Pubblicazione: (2025)

Eliminating reversals from cubical type theories
di: Cavallo, Evan, et al.
Pubblicazione: (2026)

Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory
di: Petrakis, Iosif, et al.
Pubblicazione: (2022)

First Order Logic with Fuzzy Semantics for Describing and Recognizing Nerves in Medical Images
di: Bloch, Isabelle, et al.
Pubblicazione: (2025)

A monoidal category of dependently sorted algebraic theories I: syntax
di: Almeida, Daniel
Pubblicazione: (2025)

Extensional concepts in intensional type theory, revisited
di: Kapulkin, Chris, et al.
Pubblicazione: (2023)

FILO -- automated unification in $\mathcal{FL}_0$
di: Morawska, Barbara, et al.
Pubblicazione: (2025)

Completeness of two fragments of a logic for conditional strategic reasoning
di: Li, Yinfeng, et al.
Pubblicazione: (2024)