Extracting Imperative Programs from Proofs: In-place Quicksort - Ulrich Berger (Leibniz International Proceedings in Informatics (LIPIcs), 2014)
Special Issue following the 19th International Conference on Types for Proofs and Programs (TYPES 2013).