Combining dependency, grades, and adjoint logic

Peter Hanukaev, Harley Eades

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 typ…