About: Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Creator	Wang, Peng Chlipala, Adam Delaware, Benjamin Gross, Jason Pit-Claudel, Clément
topic	covid:f531a49b32cb686067326ca6810070fee527dfe2#this
Source	PMC
abstract	We present an original approach to sound program extraction in a proof assistant, using syntax-driven automation to derive correct-by-construction imperative programs from nondeterministic functional source code. Our approach does not require committing to a single inflexible compilation strategy and instead makes it straightforward to create domain-specific code translators. In addition to a small set of core definitions, our framework is a large, user-extensible collection of compilation rules each phrased to handle specific language constructs, code patterns, or data manipulations. By mixing and matching these pieces of logic, users can easily tailor extraction to their own domains and programs, getting maximum performance and ensuring correctness of the resulting assembly code. Using this approach, we complete the first proof-generating pipeline that goes automatically from high-level specifications to assembly code. In our main case study, the original specifications are phrased to resemble SQL-style queries, while the final assembly code does manual memory management, calls out to foreign data structures and functions, and is suitable to deploy on resource-constrained platforms. The pipeline runs entirely within the Coq proof assistant, leading to final, linked assembly code with overall full-functional-correctness proofs in separation logic.
has issue date	2020-06-06(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51054-1_7
has license	no-cc
sha1sum (hex)	f531a49b32cb686067326ca6810070fee527dfe2
schema:url	https://doi.org/10.1007/978-3-030-51054-1_7
resource representing a document's title	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
has PubMed Central identifier	PMC7324049
schema:publication	Automated Reasoning
resource representing a document's body	covid:f531a49b32cb686067326ca6810070fee527dfe2#body_text
is http://vocab.deri.ie/void#inDataset of	https://covidontheweb.inria.fr:4443/about/id/http/ns.inria.fr/covid19/f531a49b32cb686067326ca6810070fee527dfe2
is schema:about of	named entity 'nondeterministic' named entity 'maximum' named entity 'specific' named entity 'ORIGINAL' named entity 'MAXIMUM' named entity 'SET' named entity 'COLLECTION' named entity 'IS A' named entity 'MIXING' named entity 'CODE' named entity 'small set' named entity 'tailor' named entity 'performance' named entity 'extraction' named entity 'domains' named entity 'Fiat' named entity 'compiler' named entity 'operational semantics' named entity 'Fiat' named entity 'syntax' named entity 'high level' named entity 'functional programs' named entity 'compiler' named entity 'Coq' named entity 'Compiler' named entity 'compiler' named entity 'database' named entity 'experimental validation' named entity 'semantics' named entity 'Coq' named entity 'Fiat' named entity 'BTree' named entity 'semantics' named entity 'Enumerate' named entity 'postcondition' named entity 'binary search trees' named entity 'memory allocation' named entity 'logic' named entity 'monads' named entity 'Fiat' named entity 'semantics' named entity 'DSLs' named entity 'data structures' named entity 'high-level' named entity 'Fiat' named entity 'impl' named entity 'source language' named entity 'program semantics' named entity 'compiler' named entity 'Fiat' named entity 'Gallina' named entity 'semantics' named entity 'recursion' named entity 'semantics' named entity 'B-tree' named entity 'kernel' named entity 'compiler' named entity 'postcondition' named entity 'Coq' named entity 'compiler' named entity 'orders of magnitude' named entity 'SQL' named entity 'PostgreSQL' named entity 'formally verified' named entity 'semantics' named entity 'Fiat' named entity 'Gallina' named entity 'code-generation' named entity 'hash table' named entity 'Fiat' named entity 'formal correctness' named entity 'database queries' named entity 'FoldL' named entity 'SQLite 3' named entity 'binary search trees' named entity 'generated code' named entity 'relational specifications'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software