Berger, Ulrich
[Author];
Seisenberger, Monika
[Author];
Woods, Gregory J. M.
[Author]
;
Ulrich Berger and Monika Seisenberger and Gregory J. M. Woods
[Contributor]
Extracting Imperative Programs from Proofs: In-place Quicksort
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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.