Imagen de Portada

A topological reading of inductive and coinductive definitions in Dependent Type Theory

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autor principal:	Sabelli, Pietro
Formato:	Preprint
Publicado:	2024
Materias:	Logic Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
por: Oda, Yukihiro, et al.
Publicado: (2021)

Primitive Recursive Dependent Type Theory
por: Buchholtz, Ulrik, et al.
Publicado: (2024)

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

Cyclic proof theory of positive inductive definitions
por: Curzi, Gianluca, et al.
Publicado: (2025)

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

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

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

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

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

Are Dependent Types in Set Theory Feasible?
por: Yang, Yunsong, et al.
Publicado: (2026)

Equiconsistency of the Minimalist Foundation with its classical version
por: Maietti, Maria Emilia, et al.
Publicado: (2024)

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

A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
por: Oda, Yukihiro, et al.
Publicado: (2022)

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

Groupoidal Realizability for Intensional Type Theory
por: Speight, Sam
Publicado: (2024)

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

Constructing (Co)inductive Types via Large Sizes
por: Laarakker, Bastiaan, et al.
Publicado: (2026)

Dependence Logics in Temporal Settings
por: Baltag, Alexandru, et al.
Publicado: (2022)

Rethinking the notion of oracle: A prequel to Lawvere-Tierney topologies for computability theorists
por: Kihara, Takayuki
Publicado: (2022)

(Pointed) Univalence in Universe Category Models of Type Theory
por: Kapulkin, Chris, et al.
Publicado: (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
por: Baader, Franz, et al.
Publicado: (2026)

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

On Small Types in Univalent Foundations
por: de Jong, Tom, et al.
Publicado: (2021)

Dependent Multiplicities in Dependent Linear Type Theory
por: Doré, Maximilian
Publicado: (2025)

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

Basis-Sensitive Quantum Typing via Realisability
por: Díaz-Caro, Alejandro, et al.
Publicado: (2025)

A Cut-free, Sound and Complete Russellian Theory of Definite Descriptions
por: Indrzejczak, Andrzej, et al.
Publicado: (2024)

Fixed Point Theorems in Computability Theory
por: Terwijn, Sebastiaan A.
Publicado: (2024)

Rings and Boolean Algebras as Algebraic Theories
por: De Faveri, Arturo
Publicado: (2025)

The Pebble-Relation Comonad in Finite Model Theory
por: Montacute, Yoàv, et al.
Publicado: (2021)

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

Proof Theory and Decision Procedures for Deontic STIT Logics
por: Lyon, Tim S., et al.
Publicado: (2024)

Universal Proof Theory, TACL 2022 Lecture Notes
por: Iemhoff, Rosalie, et al.
Publicado: (2023)

Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
por: Tabatabai, Amirhossein Akbar, et al.
Publicado: (2018)

Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
por: Tabatabai, Amirhossein Akbar, et al.
Publicado: (2018)

Correspondence and Inverse Correspondence for Input/Output Logic and Region-Based Theories of Space
por: De Domenico, Andrea, et al.
Publicado: (2024)

Gödel Incompleteness Theorem for PAC Learnable Theory from the view of complexity measurement
por: Ma, Zhifeng, et al.
Publicado: (2024)

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

Open Horn Type Theory
por: Poernomo, Iman
Publicado: (2025)