2026-08-10T20:05:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4627 2024-03-06T10:35:09Z ddc:004 open_access

Extracting Imperative Programs from Proofs: In-place Quicksort Berger, Ulrich Seisenberger, Monika Woods, Gregory J. M. Program Extraction Verification Realizability Imperative Programs In-Place Quicksort,Computational Monads Minlog 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ulrich Berger and Monika Seisenberger and Gregory J. M. Woods 2014 Is Part Of LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2013.84 urn:nbn:de:0030-drops-46274 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.84 eng https://creativecommons.org/licenses/by/3.0/legalcode