No Cover Image

Journal article 1114 views

Extracting Imperative Programs from Proofs: In-place Quicksort

Ulrich Berger Orcid Logo, Monika Seisenberger, Gregory Woods

Leibniz International Proceedings in Informatics (LIPIcs), Volume: 26, Pages: 84 - 106

Swansea University Author: Ulrich Berger Orcid Logo

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!
first_indexed 2015-05-27T02:10:53Z
last_indexed 2018-02-09T04:59:29Z
id cronfa21690
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-05-26T12:01:52.5943071</datestamp><bib-version>v2</bib-version><id>21690</id><entry>2015-05-26</entry><title>Extracting Imperative Programs from Proofs: In-place Quicksort</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><ORCID>0000-0002-7677-3582</ORCID><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2015-05-26</date><deptcode>SCS</deptcode><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.</abstract><type>Journal Article</type><journal>Leibniz International Proceedings in Informatics (LIPIcs)</journal><volume>26</volume><paginationStart>84</paginationStart><paginationEnd>106</paginationEnd><publisher/><keywords>Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort, Computational Monads</keywords><publishedDay>15</publishedDay><publishedMonth>7</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-07-15</publishedDate><doi>10.4230/LIPIcs.TYPES.2013.84</doi><url>http://drops.dagstuhl.de/opus/volltexte/2014/4627</url><notes>Special Issue following the 19th International Conference on Types for Proofs and Programs (TYPES 2013).</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-05-26T12:01:52.5943071</lastEdited><Created>2015-05-26T11:54:24.3439071</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Ulrich</firstname><surname>Berger</surname><orcid>0000-0002-7677-3582</orcid><order>1</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><order>2</order></author><author><firstname>Gregory</firstname><surname>Woods</surname><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2015-05-26T12:01:52.5943071 v2 21690 2015-05-26 Extracting Imperative Programs from Proofs: In-place Quicksort 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2015-05-26 SCS 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. Journal Article Leibniz International Proceedings in Informatics (LIPIcs) 26 84 106 Program Extraction, Verification, Realizability, Imperative Programs, In-Place Quicksort, Computational Monads 15 7 2014 2014-07-15 10.4230/LIPIcs.TYPES.2013.84 http://drops.dagstuhl.de/opus/volltexte/2014/4627 Special Issue following the 19th International Conference on Types for Proofs and Programs (TYPES 2013). COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2015-05-26T12:01:52.5943071 2015-05-26T11:54:24.3439071 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Monika Seisenberger 2 Gregory Woods 3
title Extracting Imperative Programs from Proofs: In-place Quicksort
spellingShingle Extracting Imperative Programs from Proofs: In-place Quicksort
Ulrich Berger
title_short Extracting Imperative Programs from Proofs: In-place Quicksort
title_full Extracting Imperative Programs from Proofs: In-place Quicksort
title_fullStr Extracting Imperative Programs from Proofs: In-place Quicksort
title_full_unstemmed Extracting Imperative Programs from Proofs: In-place Quicksort
title_sort Extracting Imperative Programs from Proofs: In-place Quicksort
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
Monika Seisenberger
Gregory Woods
format Journal article
container_title Leibniz International Proceedings in Informatics (LIPIcs)
container_volume 26
container_start_page 84
publishDate 2014
institution Swansea University
doi_str_mv 10.4230/LIPIcs.TYPES.2013.84
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://drops.dagstuhl.de/opus/volltexte/2014/4627
document_store_str 0
active_str 0
description 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.
published_date 2014-07-15T03:25:46Z
_version_ 1763750913625817088
score 11.013148

Similar Items