A framework for substructural type systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

49 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationESOP 2022 Proceedings
Place of PublicationCham, Switzerland
PublisherSpringer
Number of pages27
Publication statusE-pub ahead of print - 7 Apr 2022
EventEuropean Symposium on Programming 2022 - https://etaps.org/2022/esop, Munich, Germany
Duration: 2 Apr 20227 Apr 2022

Publication series

NameLecture Notes in Computer Science

Conference

ConferenceEuropean Symposium on Programming 2022
Abbreviated titleESOP 2022
Country/TerritoryGermany
CityMunich
Period2/04/227/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.

Cite this