Program extraction for mutable arrays

DOI10.1007/978-3-319-90686-7_4OpenAlexW2800345163MaRDI QIDQ1648867FDOQ1648867

Authors Kazuhiko Sakaguchi 

Publication date 9 July 2018

Full work available at URL https://doi.org/10.1007/978-3-319-90686-7_4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Analyzing Array Manipulating Programs by Program Transformation
• Program Extraction in Constructive Analysis
• Program extraction from nested definitions
• Algorithmic analysis of array-accessing programs
• Algorithmic Analysis of Array-Accessing Programs
• A Binding Scope Analysis for Generic Programs on Arrays
• Extracting non-deterministic concurrent programs
• Program extraction from large proof developments
• Program extraction in exact real arithmetic

Cited In (4)

• Extracting imperative programs from proofs: In-place Quicksort
• Title not available (Why is no real title available?)
• Towards a practical library for monadic equational reasoning in Coq
• Analyzing Array Manipulating Programs by Program Transformation

Uses Software

• Coq
• Isabelle/HOL
• Coq/SSReflect
• Ynot

This page was built for publication: Program extraction for mutable arrays

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1648867)