Reference. Foundations of Substructural Dependent Type Theory

This paper presents preliminary work on a general system for integrating dependent types into substructural type systems such as linear logic and linear type theory. Prior work on this front has generally managed to deliver type systems possessing either syntax or semantics inclusive of certain practical applications, but has struggled to combine these all in one and the same system. Toward resolving this difficulty, I propose a novel categorical interpretation of substructural dependent types, analogous to the use of monoidal categories as models of linear and ordered logic, that encompasses a wide class of mathematical and computational examples. On this basis, I develop a general framework for substructural dependent type theories, and proceed to prove some essential metatheoretic properties thereof. As an application of this framework, I show how it can be used to construct a type theory that satisfactorily addresses the problem of effectively representing cut admissibility for linear sequent calculus in a logical framework.

Cite

Cite as @aberle-2024-foundations (helia, typst) · \cite{aberle-2024-foundations} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{aberle-2024-foundations,
  author = {CB Aberle},
  title = {Foundations of Substructural Dependent Type Theory},
  year = {2024},
  month = {1},
  eprint = {2401.15258},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 7 lines
aberle-2024-foundations:
  type: misc
  title: Foundations of Substructural Dependent Type Theory
  author: Aberle, CB
  date: 2024-01
  serial-number:
    arxiv: '2401.15258'
Cites 14 works (5 here)
With notes (5)

Normalization for Cubical Type Theory sterling_angiuli_2021

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of β/η-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.
Web

Syntax and Semantics of Quantitative Type Theory atkey-2018-syntax

DOI

I Got Plenty o’ Nuttin’ mcbride-2016-i

DOI

Integrating Linear and Dependent Types krishnaswami_integrating_2015

In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.
PDF · DOI · pldb

Linear logic girard_linear_1987

The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI
External (9)
aberle-2024-foundations reference entries/refs/aberle-2024-foundations/aberle-2024-foundations.hel