Extracting imperative programs from proofs: In-place Quicksort

DOI10.4230/LIPICS.TYPES.2013.84MaRDI QIDQ2968412zbMATH OpenOpenAlexFDO

Authors Ulrich Berger, Monika Seisenberger, Gregory J. M. Woods

Publication date 13 March 2017

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2014/4627/pdf/p084-05-berger.pdf

zbMATH Keywords

verificationrealizabilitycomputational monadsprogram extractionimperative programsMinlogIn-place Quicksort

Mathematics Subject Classification ID

Searching and sorting (68P10) Functional programming and lambda calculus (68N18)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• Proofs and programs: A naïve approach to program extraction
• Program extraction for mutable arrays
• scientific article; zbMATH DE number 2003148
• scientific article; zbMATH DE number 2003158

Cited in

(5)

• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Proving Quicksort Correct in Event-B

Describes a project that uses

Uses Software

• Minlog

This page was built for publication: Extracting imperative programs from proofs: In-place Quicksort

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