Extracting Imperative Programs from Proofs: In-place Quicksort. - Ulrich Berger 001; Monika Seisenberger; Gregory J. M. Woods (TYPES, 2013)