Projects per year
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.
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.
Original language | English |
---|---|
Title of host publication | ESOP 2022 Proceedings |
Place of Publication | Cham, Switzerland |
Publisher | Springer |
Number of pages | 27 |
Publication status | E-pub ahead of print - 7 Apr 2022 |
Event | European Symposium on Programming 2022 - https://etaps.org/2022/esop, Munich, Germany Duration: 2 Apr 2022 → 7 Apr 2022 |
Publication series
Name | Lecture Notes in Computer Science |
---|
Conference
Conference | European Symposium on Programming 2022 |
---|---|
Abbreviated title | ESOP 2022 |
Country/Territory | Germany |
City | Munich |
Period | 2/04/22 → 7/04/22 |
Keywords
- formalised syntax
- substructural types
- mechanised metatheory
- quantitative typing
Fingerprint
Dive into the research topics of 'A framework for substructural type systems'. Together they form a unique fingerprint.Projects
- 1 Finished
-
AISEC: AI Secure and Explainable by Construction
Atkey, B. (Principal Investigator)
EPSRC (Engineering and Physical Sciences Research Council)
1/06/20 → 9/06/24
Project: Research