Cover Image

Are Dependent Types in Set Theory Feasible?

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Yang, Yunsong, Guilloud, Simon, Kunčak, Viktor
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Orthologic Type Systems
by: Guilloud, Simon, et al.
Published: (2025)

Interpolation and Quantifiers in Ortholattices
by: Guilloud, Simon, et al.
Published: (2025)

LISA -- A Modern Proof System
by: Guilloud, Simon, et al.
Published: (2025)

Mechanized HOL Reasoning in Set Theory
by: Guilloud, Simon, et al.
Published: (2024)

Orthologic for SAT Solving
by: de Haldat, Vladislas, et al.
Published: (2026)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
by: Cailler, Julie, et al.
Published: (2025)

Verified and Optimized Implementation of Orthologic Proof Search
by: Guilloud, Simon, et al.
Published: (2025)

Primitive Recursive Dependent Type Theory
by: Buchholtz, Ulrik, et al.
Published: (2024)

Non-Derivability Results in Polymorphic Dependent Type Theory
by: Geuvers, Herman
Published: (2026)

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
by: Gratzer, Daniel, et al.
Published: (2024)

A topological reading of inductive and coinductive definitions in Dependent Type Theory
by: Sabelli, Pietro
Published: (2024)

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
by: Mannucci, Mirco A., et al.
Published: (2026)

Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe
by: Takahashi, Yuta
Published: (2024)

Dependence Logics in Temporal Settings
by: Baltag, Alexandru, et al.
Published: (2022)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

The Groupoid-Syntax of Type Theory is a Set
by: Altenkirch, Thorsten, et al.
Published: (2025)

Dependent Multiplicities in Dependent Linear Type Theory
by: Doré, Maximilian
Published: (2025)

A Foundation for Differentiable Logics using Dependent Type Theory
by: Affeldt, Reynald, et al.
Published: (2026)

Feasibly Constructive Proof of Schwartz-Zippel Lemma and the Complexity of Finding Hitting Sets
by: Atserias, Albert, et al.
Published: (2024)

Characterizing Sets of Theories That Can Be Disjointly Combined
by: Przybocki, Benjamin, et al.
Published: (2025)

The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
by: Baader, Franz, et al.
Published: (2026)

DEKL 2.0: Trace-Indexed Knowledge Evolution in Dependent Type Theory
by: Peng, Chen
Published: (2026)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by: Hermes, Marc, et al.
Published: (2023)

A Naive Encoding of Russell's Paradox in Type Theory
by: Qu, Zhuoyuan
Published: (2025)

A Graded Modal Dependent Type Theory with Erasure, Formalized
by: Abel, Andreas, et al.
Published: (2026)

Groupoidal Realizability for Intensional Type Theory
by: Speight, Sam
Published: (2024)

Coslice Colimits in Homotopy Type Theory
by: Hart, Perry, et al.
Published: (2024)

Foundations of Substructural Dependent Type Theory
by: Aberlé, C. B.
Published: (2024)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
by: Mannucci, Mirco A., et al.
Published: (2025)

Hammering Higher Order Set Theory
by: Brown, Chad E., et al.
Published: (2025)

Open Horn Type Theory
by: Poernomo, Iman
Published: (2025)

(Pointed) Univalence in Universe Category Models of Type Theory
by: Kapulkin, Chris, et al.
Published: (2025)

Intersection Types via Finite-Set Declarations
by: Kamareddine, Fairouz, et al.
Published: (2024)

A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
by: Bezem, Marc, et al.
Published: (2026)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
by: Hu, Jason Z. S., et al.
Published: (2024)

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

Nominal Type Theory by Nullary Internal Parametricity
by: Van Muylder, Antoine, et al.
Published: (2025)

A Judgmental Construction of Directed Type Theory
by: Neumann, Jacob
Published: (2025)

Dependent Type Refinements for Futures
by: Somayyajula, Siva, et al.
Published: (2023)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
by: Niederhauser, Johannes, et al.
Published: (2024)