×

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].

MSC:

68N18 Functional programming and lambda calculus
68P10 Searching and sorting
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Minlog
PDFBibTeX XMLCite
Full Text: DOI