This HTML5 document contains 30 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n22doi:10.1007/
dctermshttp://purl.org/dc/terms/
n11https://kar.kent.ac.uk/84636/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n4http://purl.org/ontology/bibo/status/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n13https://kar.kent.ac.uk/id/eprint/84636#
n9https://kar.kent.ac.uk/id/subject/
n18https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n5http://eprints.org/ontology/
n8https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n12https://kar.kent.ac.uk/id/publication/
n20https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n6https://kar.kent.ac.uk/id/document/
n19https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n17https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n15https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:84636
rdf:type
bibo:AcademicArticle bibo:Article n5:EPrint n5:ConferenceItemEPrint
rdfs:seeAlso
n11:
owl:sameAs
n22:978-3-030-68446-4_8
n5:hasDocument
n6:3239612 n6:3239617 n6:3239629 n6:3239630 n6:3239631 n6:3239632
n5:hasPublished
n6:3239612
dc:hasVersion
n6:3239612
dcterms:title
Resourceful program synthesis from graded linear types
wdrs:describedby
n17:export_kar_RDFN3.n3 n18:export_kar_RDFN3.n3
dcterms:date
2021-02-13
dcterms:creator
n15:ext-16f64573fce23d2dfe3886ba83fcb5f6 n15:ext-d.a.orchard@kent.ac.uk
bibo:status
n4:peerReviewed n4:published
dcterms:publisher
n20:ext-1c5ddec173ca8cdfba8b274309638579
bibo: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.
dcterms:isPartOf
n12:ext-03029743 n19:repository
dcterms:subject
n9:QA76
bibo:authorList
n13:authors
bibo:presentedAt
n8:ext-8b798668178eecde968eb3781ae8d050
bibo:volume
12561