Berger, Ulrich; Seisenberger, Monika; Woods, Gregory J. M. Extracting imperative programs from proofs: In-place Quicksort. (English) Zbl 1359.68042 Matthes, Ralph (ed.) et al., 19th international conference on types for proofs and programs, TYPES 2013, Toulouse, France, April 22–26, 2013. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-72-9). LIPIcs – Leibniz International Proceedings in Informatics 26, 84-106 (2014). Summary: The process of program extraction is primarily associated with functional programs with less focus on imperative program extraction. In this paper we consider a standard problem for imperative programming: In-place Quicksort. We formalize a proof that every array of natural numbers can be sorted and apply a realizability interpretation to extract a program from the proof. Using monads we are able to exhibit the inherent imperative nature of the extracted program. We see this as a first step towards an automated extraction of imperative programs. The case study is carried out in the interactive proof assistant Minlog.For the entire collection see [Zbl 1294.68024]. Cited in 3 Documents MSC: 68N18 Functional programming and lambda calculus 68P10 Searching and sorting 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:program extraction; verification; realizability; imperative programs; In-place Quicksort; computational monads; Minlog Software:Minlog PDFBibTeX XMLCite \textit{U. Berger} et al., LIPIcs -- Leibniz Int. Proc. Inform. 26, 84--106 (2014; Zbl 1359.68042) Full Text: DOI