Abstract
Mechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on structurality of the type system — that weakening, contraction, and exchange are admissible and variables can be used unrestrictedly once assumed. Linear logic, and many related subsequent systems, provide motivations for breaking some of these assumptions.
We present a framework for mechanising the metatheory of certain substructural type systems, in a style resembling mechanised metatheory of structural type systems. The framework covers a wide range of simply typed syntaxes with semiring usage annotations, via a metasyntax of typing rules. The metasyntax for the premises of a typing rule is related to bunched logic, featuring both sharing and separating conjunction, roughly corresponding to the additive and multiplicative features of linear logic. We use the uniformity of syntaxes to derive type system-generic renaming, substitution, and a form of linearity checking.
James Wood is supported by an EPSRC Studentship. Robert Atkey is supported by EPSRC grant EP/T026960/1.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A Core Calculus of Dependency. In: POPL ’99, pp. 147–160 (1999)
Abel, A., Bernardy, J.P.: A unified view of modalities in type systems. Proc. ACM Program. Lang. 4(ICFP) (Aug 2020), https://doi.org/10.1145/3408972, URL https://doi.org/10.1145/3408972
Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31, e22 (2021), https://doi.org/10.1017/S0956796820000076, URL https://doi.org/10.1017/S0956796820000076
Atkey, R.: The syntax and semantics of quantitative type theory. In: LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9–12, 2018, Oxford, United Kingdom (2018), https://doi.org/10.1145/3209108.3209189
Atkey, R., Wood, J.: Context constrained computation. In: 3rd Workshop on Type-Driven Development (TyDe ’18), Extended Abstract (2018)
Benton, P.: A mixed linear and non-linear logic: Proofs, terms and models. pp. 121–135, Springer-Verlag (1994)
Brunel, A., Gaboardi, M., Mazza, D., Zdancewic, S.: A Core Quantitative Coeffect Calculus. In: ESOP 2014, pp. 351–370 (2014)
Curien, P.L., Herbelin, H.: The duality of computation. SIGPLAN Not. 35(9), 233–243 (Sep 2000), ISSN 0362–1340, https://doi.org/10.1145/357766.351262, URL https://doi.org/10.1145/357766.351262
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp. 193–202 (1999), https://doi.org/10.1109/LICS.1999.782615
Ghica, D.R., Smith, A.I.: Bounded linear types in a resource semiring. In: ESOP 2014, pp. 331–350 (2014)
Girard, J.Y.: Linear logic. Theor. Comp. Sci. 50, 1–101 (1987)
Herbelin, H.: C’est maintenant qu’on calcule, au cœur de la dualité. Habilitation (2005)
Licata, D.R., Shulman, M., Riley, M.: A fibrational framework for substructural and modal logics. In: FSCD 2017, pp. 25:1–25:22 (2017), https://doi.org/10.4230/LIPIcs.FSCD.2017.25
Lovas, W., Crary, K.: Structural normalization for classical natural deduction (2006)
McBride, C.: Type-preserving renaming and substitution (2005), URL http://www.strictlypositive.org/ren-sub.pdf
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. BULLETIN OF SYMBOLIC LOGIC 5(2), 215–244 (1999)
Orchard, D.A., Liepelt, V., Eades, H.: Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages 3 (June 2019)
Petricek, T., Orchard, D.A., Mycroft, A.: Coeffects: a calculus of context-dependent computation. In: ICFP 2014, pp. 123–135 (2014)
Reed, J., Pierce, B.C.: Distance makes the types grow stronger. In: Hudak, P., Weirich, S. (eds.) ICFP 2010, pp. 157–168 (2010)
Rouvoet, A., Bach Poulsen, C., Krebbers, R., Visser, E.: Intrinsically-typed definitional interpreters for linear, session-typed languages. In: CPP 2020, pp. 284–298 (2020), ISBN 9781450370974, https://doi.org/10.1145/3372885.3373818
Wood, J., Atkey, R.: A linear algebra approach to linear metatheory. arXiv preprint arXiv:2005.02247 (2020)
Wood, J., Atkey, R.: lamudri/generic-lr (Jan 2022), https://doi.org/10.5281/zenodo.5920051, URL https://doi.org/10.5281/zenodo.5920051
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Wood, J., Atkey, R. (2022). A Framework for Substructural Type Systems. In: Sergey, I. (eds) Programming Languages and Systems. ESOP 2022. Lecture Notes in Computer Science, vol 13240. Springer, Cham. https://doi.org/10.1007/978-3-030-99336-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-99336-8_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99335-1
Online ISBN: 978-3-030-99336-8
eBook Packages: Computer ScienceComputer Science (R0)