Combining dependency, grades, and adjoint logic
Logic in Computer Science
2023-07-20 v1
Abstract
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.
Keywords
Cite
@article{arxiv.2307.09563,
title = {Combining dependency, grades, and adjoint logic},
author = {Peter Hanukaev and Harley Eades},
journal= {arXiv preprint arXiv:2307.09563},
year = {2023}
}