No Cover Image

Journal article 440 views

Extracting Imperative Programs from Proofs: In-place Quicksort / Ulrich, Berger

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...

Full description

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: College of Science
Start Page: 84
End Page: 106