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
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.
Syntax and Semantics of Quantitative Type Theory atkey-2018-syntax
I Got Plenty o’ Nuttin’ mcbride-2016-i
Integrating Linear and Dependent Types krishnaswami_integrating_2015
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.
External (9)
- Effective Quantum Certification via Linear Homotopy Types (2023)
- The Para Construction as a Distributive Law (2022)
- A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory (2022)
- Multimodal Dependent Type Theory (2020)
- A Hybrid Logical Framework (2009)
- A Linear Logical Framework (2002)
- Comprehension categories and the semantics of type dependency (1993)
- Telescopic mappings in typed lambda calculus (1991)
- An Intuitionistic Theory of Types: Predicative Part (1975)