Bibliography · Foundations and Logic

Foundations of Substructural Dependent Type Theory

Article Formal Antecedent Foundations and Logic

Citation

Daniel Gratzer and Jonathan Sterling. (2024). Foundations of Substructural Dependent Type Theory.

Publisher

Why this reference is included

Gratzer and Sterling’s paper Foundations of Substructural Dependent Type Theory (2024) is one of the program’s working technical references. Cited across Book I (Categorical Foundations), Part 18, Chapter Star-Autonomous Categories and the Diagonal Barrier; Book I (Categorical Foundations), Part 18, Chapter The Enrichment Frontier — the central framing is “Substructural dependent type theory : dependent types with monoidal (not cartesian closed) models, supporting resource tracking within a dependently typed framework”.

Cited in

  • Book I — Categorical Foundations Part 18
    Chapter Star-Autonomous Categories and the Diagonal Barrier
    Substructural dependent type theory : dependent types with monoidal (not cartesian closed) models, supporting resource tracking within a dependently typed framework
  • Book I — Categorical Foundations Part 18
    Chapter The Enrichment Frontier
    Resource-sensitive type theory exists (graded modal DTT , substructural DTT )
  • Book I — Categorical Foundations Part 18
    Chapter The Enrichment Frontier
    The substructural dependent type theory of constructs monoidal (not CCC) models for dependent types, replacing cartesian products with tensor products

Bibliographic Details

BibTeX KeySubstructuralDTT2024
AuthorsDaniel Gratzer and Jonathan Sterling
Year
TypeArticle