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 (ICFP). Article Number 110. E-ISSN 2475-1421. (doi:10.1145/3341714) (KAR id:74450)

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


Download (1MB) Preview
[thumbnail of (with appendices)]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Dominic Orchard
Date Deposited: 18 Jun 2019 15:27 UTC
Last Modified: 24 Nov 2021 10:41 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):

Downloads

Downloads per month over past year