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