Skip to main content

Quantitative program reasoning with graded modal types

Orchard, Dominic A., Liepelt, Vilem, Eades, Harley (2019) Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages, 3 . E-ISSN 2475-1421. (doi:10.1145/3341714) (KAR id:74450)

PDF ((with appendices)) Author's Accepted Manuscript
Language: English


Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (1MB) Preview
Official URL
http://dx.doi.org/10.1145/3341714

Abstract

In programming, data is often considered to be infinitely copiable, arbitrarily discardable, and universally unconstrained. However this view is naive: some data encapsulates resources that are subject to protocols (e.g., file and device handles, channels); some data should not be arbitrarily copied or communicated (e.g., private data). Linear types provide a partial remedy by delineating data in two camps: "resources" to be used but never copied or discarded, and unconstrained values. However, this binary distinction is too coarse-grained. Instead, we propose the general notion of graded modal types, which in combination with linear and indexed types, provides an expressive type theory for enforcing fine-grained resource-like properties of data. We present a type system drawing together these aspects (linear, graded, and indexed) embodied in a fully-fledged functional language implementation, called Granule. We detail the type system, including its metatheoretic properties, and explore examples in the concrete language. This work advances the wider goal of expanding the reach of type systems to capture and verify a broader set of program properties.

Item Type: Article
DOI/Identification number: 10.1145/3341714
Uncontrolled keywords: graded modal types, linear types, coeffects, implementation
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Dominic Orchard
Date Deposited: 18 Jun 2019 15:27 UTC
Last Modified: 07 Aug 2020 13:07 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/74450 (The current URI for this page, for reference purposes)
Orchard, Dominic A.: https://orcid.org/0000-0002-7058-7842
Liepelt, Vilem: https://orcid.org/0000-0002-2198-1819
Eades, Harley: https://orcid.org/0000-0001-8474-5971
  • Depositors only (login required):