Extracting imperative programs from proofs: In-place Quicksort

DOI10.4230/LIPICS.TYPES.2013.84zbMATH Open1359.68042OpenAlexW1522541548MaRDI QIDQ2968412FDOQ2968412

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

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

zbMATH Keywords

verificationrealizabilitycomputational monadsprogram extractionimperative programsMinlogIn-place Quicksort

Mathematics Subject Classification ID

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

Cited In (5)

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

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)