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

computational monadsimperative programsIn-place QuicksortMinlogprogram extractionrealizabilityverification

Mathematics Subject Classification ID

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

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)

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

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)