Journal article 1114 views
Extracting Imperative Programs from Proofs: In-place Quicksort
,
Monika Seisenberger,
Gregory Woods
Leibniz International Proceedings in Informatics (LIPIcs), Volume: 26, Pages: 84 - 106
Swansea University Author:
Ulrich Berger
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.4230/LIPIcs.TYPES.2013.84
Abstract
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...
| Published in: | Leibniz International Proceedings in Informatics (LIPIcs) |
|---|---|
| Published: |
2014
|
| Online Access: |
http://drops.dagstuhl.de/opus/volltexte/2014/4627 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa21690 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
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. |
|---|---|
| Item Description: |
Special Issue following the 19th International Conference on Types for Proofs and Programs (TYPES 2013). |
| Keywords: |
Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort, Computational Monads |
| College: |
Faculty of Science and Engineering |
| Start Page: |
84 |
| End Page: |
106 |