School of Computing

Oct 12
15:00 - 16:00
PLAS: Jack Hughes
PLAS Group Seminar
Resourceful Program Synthesis from Graded Linear Types

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: howdoes 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 lineartype 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

Work with Dominic Orchard.

Location

anywhere,
via Teams.
United Kingdom

Details

Contact: O.Chitil
E: oc@kent.ac.uk
School of Computing

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 14/08/2015