Skip to main content
Kent Academic Repository

Resourceful program synthesis from graded linear types

Hughes, Jack, Orchard, Dominic A. (2021) Resourceful program synthesis from graded linear types. Lecture Notes in Computer Science, 12561 . ISSN 0302-9743. (doi:10.1007/978-3-030-68446-4_8) (KAR id:84636)

Abstract

Linear types provide a way to constrain programs by specifying that some values must be used exactly once. Recent work on graded modal types augments and refines this notion, enabling fine-grained, quantitative specification of data use in programs. The information provided by graded modal types appears to be useful for type-directed program synthesis, where these additional constraints can be used to prune the search space of candidate programs. We explore one of the major implementation challenges of a synthesis algorithm in this setting: how does the synthesis algorithm efficiently ensure that resource constraints are satisfied throughout program generation? We provide two solutions to this resource management problem, adapting Hodas and Miller’s input-output model of linear context management to a graded modal linear type theory. We evaluate the performance of both approaches via their implementation as a program synthesis tool for the programming language Granule, which provides linear and graded modal typing.

Item Type: Article
DOI/Identification number: 10.1007/978-3-030-68446-4_8
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: 30 Nov 2020 11:05 UTC
Last Modified: 15 Nov 2022 15:42 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/84636 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.