About: Quantitative program reasoning with graded modal types

Not logged in : Login

(Sponging disallowed)

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

About: Quantitative program reasoning with graded modal 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/ArticleEPrint http://eprints.org/ontology/EPrint Article Academic Article
seeAlso	HTML Summary of #74450 Quantitative program reasoning with graded modal types
sameAs	Quantitative program reasoning with graded modal types
http://eprints.org/ontology/hasAccepted	Quantitative program reasoning with graded modal types (PDF)
http://eprints.org/ontology/hasDocument	Quantitative program reasoning with graded modal types (PDF) Quantitative program reasoning with graded modal types (Other) Quantitative program reasoning with graded modal types (Other) Quantitative program reasoning with graded modal types (Other) Quantitative program reasoning with graded modal types (Other) Quantitative program reasoning with graded modal types (Other)
dc:hasVersion	Quantitative program reasoning with graded modal types (PDF)
Title	Quantitative program reasoning with graded modal types
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3
Date	2019-08-01
Creator	Dominic A. Orchard Harley Eades Vilem Liepelt
status	peer reviewed published
Publisher	ACM
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.
Is Part Of	Proceedings of the ACM on Programming Languages https://kar.kent.ac.uk/id/repository
Subject	QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/74450#authors
issue	ICFP
volume	3
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #74450 Quantitative program reasoning with graded modal 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, 15 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software