@inproceedings{e9d573d70df749bf9fe8cadfec170e0f,
title = "Combining Dependency, Grades, and Adjoint Logic",
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 = "adjoint logic, dependent types, graded types, linear logic, resource tracking, semantics",
author = "Peter Hanukaev and Harley Eades",
note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.; 8th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe 2023, co-located with the International Conference on Functional Programming, ICFP 2023 ; Conference date: 04-09-2023",
year = "2023",
month = aug,
day = "30",
doi = "10.1145/3609027.3609408",
language = "English (US)",
series = "TyDe 2023 - Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development, Co-located with ICFP 2023",
publisher = "Association for Computing Machinery, Inc",
pages = "58--70",
editor = "Youyou Cong and Pierre-Evariste Dagand",
booktitle = "TyDe 2023 - Proceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development, Co-located with ICFP 2023",
}