Cover Image

A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ceulemans, Joris, Nuyts, Andreas, Devriese, Dominique
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Transpension: The Right Adjoint to the Pi-type
by: Nuyts, Andreas, et al.
Published: (2020)

The Transpension Type: Technical Report
by: Nuyts, Andreas
Published: (2020)

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

On the Completeness of Interpolation Algorithms
by: Hetzl, Stefan, et al.
Published: (2024)

Type Theory with Single Substitutions
by: Kaposi, Ambrus, et al.
Published: (2025)

Sound and Complete Invariant-Based Heap Encodings (Technical Report)
by: Esen, Zafer, et al.
Published: (2025)

Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
by: Marin, Sonia, et al.
Published: (2025)

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

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

Sound and Complete Proof Rules for Probabilistic Termination
by: Majumdar, Rupak, et al.
Published: (2024)

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

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

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

A Syntactic Approach to Computing Complete and Sound Abstraction in the Situation Calculus
by: Fang, Liangda, et al.
Published: (2024)

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

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

Technical Report: Time-Bounded Resilience
by: Kirigin, Tajana Ban, et al.
Published: (2024)

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

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

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

The Power of Regular Constraint Propagation (Technical Report)
by: Hague, Matthew, et al.
Published: (2025)

A Complete Finite Axiomatisation of the Equational Theory of Common Meadows
by: Bergstra, Jan A, et al.
Published: (2023)

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

On the Decidability of Monadic Theories of Arithmetic Predicates
by: Berthé, Valérie, et al.
Published: (2024)

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

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

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

Completions of Kleene's second model
by: Terwijn, Sebastiaan A.
Published: (2023)

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

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

Separation and Encodability in Mixed Choice Multiparty Sessions (Technical Report)
by: Peters, Kirstin, et al.
Published: (2024)

The Modal Cube Revisited: Semantics without Worlds (Technical Report)
by: Leme, Renato, et al.
Published: (2025)

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

Complete and Terminating Tableau Calculus for Undirected Graph
by: Nishimura, Yuki, et al.
Published: (2024)

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory
by: Schewe, Klaus-Dieter, et al.
Published: (2025)

The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
by: Nakamura, Yoshiki
Published: (2025)

Deciding Boolean Separation Logic via Small Models (Technical Report)
by: Dacík, Tomáš, et al.
Published: (2024)

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

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