Cited By
View all- Marshall DOrchard D(2024)Functional Ownership through Fractional UniquenessProceedings of the ACM on Programming Languages10.1145/36498488:OOPSLA1(1040-1070)Online publication date: 29-Apr-2024
Combining Dependency, Grades, and Adjoint Logic
Pages 58 - 70
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.
References
[1]
Robert Atkey. 2018. Syntax and Semantics of Quantitative Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. ACM. https://doi.org/10.1145/3209108.3209189
[2]
P. N. Benton. 1995. A mixed linear and non-linear logic: Proofs, terms and models. In Computer Science Logic. Springer Berlin Heidelberg, 121–135. https://doi.org/10.1007/bfb0022251
[3]
Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010 - Concurrency Theory, Paul Gastin and François Laroussinie (Eds.) (Lecture Notes in Computer Science, Vol. 6269). Springer Berlin Heidelberg, 222–236. https://doi.org/10.1007/978-3-642-15375-4_16
[4]
Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. 2021. A graded dependent type system with a usage-aware semantics. Proceedings of the ACM on Programming Languages, 5, POPL (2021), jan, 1–32. https://doi.org/10.1145/3434331
[5]
Peter Dybjer. 1996. Internal type theory. In Types for Proofs and Programs, Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 120–134. isbn:978-3-540-70722-6 https://doi.org/10.1007/3-540-61780-9_66
[6]
Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science, 50, 1 (1987), 1–101. https://doi.org/10.1016/0304-3975(87)90045-4
[7]
Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. 1992. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical Computer Science, 97, 1 (1992), 1–66. https://doi.org/10.1016/0304-3975(92)90386-T
[8]
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. 2020. Multimodal Dependent Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20). Association for Computing Machinery, New York, NY, USA. 492–506. isbn:9781450371049 https://doi.org/10.1145/3373718.3394736
[9]
Peter Hanukaev and Harley Eades III. 2023. Combining Dependency, Grades, and Adjoint Logic (extended version). https://doi.org/10.48550/arXiv.2307.09563
[10]
Bartholomeus Paulus Franciscus Jacobs. 1991. Categorical type theory. Nijmegen. PhD thesis
[11]
Shin-ya Katsumata. 2018. A Double Category Theoretic Analysis of Graded Linear Exponential Comonads. In Lecture Notes in Computer Science. Springer International Publishing, 110–127. https://doi.org/10.1007/978-3-319-89366-2_6
[12]
Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. ACM SIGPLAN Notices, 50, 1 (2015), may, 17–30. https://doi.org/10.1145/2775051.2676969
[13]
Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Dale Miller (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 84). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 25:1–25:22. isbn:978-3-95977-047-7 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSCD.2017.25
[14]
Benjamin Moon, Harley Eades III, and Dominic Orchard. 2021. Graded Modal Dependent Type Theory. In Programming Languages and Systems. Springer International Publishing, 462–490. https://doi.org/10.1007/978-3-030-72019-3_17
[15]
Bengt Nordstrom, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press, USA.
[16]
Peter O’Hearn, John Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In Computer Science Logic, Laurent Fribourg (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–19. https://doi.org/10.1007/3-540-44802-0_1
[17]
Peter W. O’Hearn and David J. Pym. 1999. The Logic of Bunched Implications. The Bulletin of Symbolic Logic, 5, 2 (1999), 215–244. https://doi.org/10.2307/421090
[18]
Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. Quantitative Program Reasoning with Graded Modal Types. Proc. ACM Program. Lang., 3, ICFP (2019), Article 110, jul, 30 pages. https://doi.org/10.1145/3341714
[19]
Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed. 2018. Adjoint Logic. Unpublished Draft: https://www.cs.cmu.edu/ fp/papers/adjoint18b.pdf
[20]
Victoria Vollmer, Harley Eades III, Daniel Marshall, and Dominic Orchard. [n. d.]. A Mixed Linear and Graded Logic: Proofs, Terms and Models. forthcoming
[21]
James Wood and Robert Atkey. 2022. A Framework for Substructural Type Systems. In Programming Languages and Systems, Ilya Sergey (Ed.). Springer International Publishing, Cham. 376–402. isbn:978-3-030-99336-8 https://doi.org/10.1007/978-3-030-99336-8_14
Index Terms
- Combining Dependency, Grades, and Adjoint Logic
Recommendations
The decidability of the intensional fragment of classical linear logic
Intensional classical linear logic (MELL) is proved decidable.Intensional interlinear logic (RLL) is proved decidable.We adapt Kripke's method used to prove decidability for some relevance logics.The semi-relevant RLL emerges as a logic superior to MELL ...
On abstract resource semantics and computability logic
We show that the uniform validity is equivalent to the non-uniform validity for Blass' semantics of [A. Blass, A game semantics for linear logic, Ann. Pure Appl. Logic 56 (1992) 183-220]. We present a shorter proof (than that of [G. Japaridze, The ...
Nominal Lambda Calculus: An Internal Language for FM-Cartesian Closed Categories
Reasoning about atoms (names) is difficult. The last decade has seen the development of numerous novel techniques. For equational reasoning, Clouston and Pitts introduced Nominal Equational Logic (NEL), which provides judgements of equality and ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
August 2023
70 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 August 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
TyDe '23
Sponsor:
TyDe '23: 8th ACM SIGPLAN International Workshop on Type-Driven Development
September 4, 2023
WA, Seattle, USA
Upcoming Conference
ICFP '25
- Sponsor:
- sigplan
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 184Total Downloads
- Downloads (Last 12 months)152
- Downloads (Last 6 weeks)20
Reflects downloads up to 22 Nov 2024
Other Metrics
Citations
Cited By
View all- Marshall DOrchard D(2024)Functional Ownership through Fractional UniquenessProceedings of the ACM on Programming Languages10.1145/36498488:OOPSLA1(1040-1070)Online publication date: 29-Apr-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in