About: Resourceful program synthesis from graded linear types

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Resourceful program synthesis from graded linear types Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:AcademicArticle, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/ConferenceItemEPrint http://eprints.org/ontology/EPrint Article Academic Article
seeAlso	HTML Summary of #84636 Resourceful program synthesis from graded linear types
sameAs	Resourceful program synthesis from graded linear types
http://eprints.org/ontology/hasDocument	Resourceful program synthesis from graded linear types (PDF) Resourceful program synthesis from graded linear types (Other) Resourceful program synthesis from graded linear types (Other) Resourceful program synthesis from graded linear types (Other) Resourceful program synthesis from graded linear types (Other) Resourceful program synthesis from graded linear types (Other)
http://eprints.org/ontology/hasPublished	Resourceful program synthesis from graded linear types (PDF)
dc:hasVersion	Resourceful program synthesis from graded linear types (PDF)
Title	Resourceful program synthesis from graded linear types
described by	https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2021-02-13
Creator	Jack Hughes Dominic A. Orchard
status	peer reviewed published
Publisher	Springer
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.
Is Part Of	Financial Cryptography and Data Security https://kar.kent.ac.uk/id/repository
Subject	QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/84636#authors
presented at	International Symposium on Logic-Based Program Synthesis and Transformation
volume	12561
is topic of	https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #84636 Resourceful program synthesis from graded linear types

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 16 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software