ICFP 2023 (series) / TyDe 2023 (series) / TyDe 2023 /
Combining Dependency, Grades, and Adjoint Logic
We propose two new dependent type systems. The first, is a dependent
graded/linear type system where a graded dependent type system is
connected via modal operators to a linear type system in the style of
Linear/Non-linear logic. We then generalize this system to support
many graded systems connected by many modal operators through the
introduction of modes from Adjoint Logic. Finally, we prove several
meta-theoretic properties of these two systems including graded
substitution.
Mon 4 SepDisplayed time zone: Pacific Time (US & Canada) change
Mon 4 Sep
Displayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | TyDe: Type-Driven TypesTyDe at St Helens Chair(s): Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Japan | ||
11:00 22mTalk | A Calculus of Inductive Linear Constructions TyDe DOI | ||
11:22 22mTalk | A Dependently Typed Language with Dynamic Equality TyDe Mark Lemay Autodesk, Qiancheng Fu Boston University, William Blair Boston University, Cheng Zhang Boston University, Hongwei Xi Boston University DOI | ||
11:45 22mTalk | Combining Dependency, Grades, and Adjoint Logic TyDe DOI | ||
12:07 22mTalk | Infix-Extensible Record Types for Tabular DataRecorded TyDe DOI | ||