No Cover Image

Journal article 1327 views

Proofs, Programs, Processes

Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo

Theory of Computing Systems, Volume: 51, Issue: 3, Pages: 313 - 329

Swansea University Authors: Ulrich Berger Orcid Logo, Monika Seisenberger Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

DOI (Published version): 10.1007/s00224-011-9325-8

Abstract

The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that...

Full description

Published in: Theory of Computing Systems
ISSN: 1432-4350 1433-0490
Published: 2012
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa7438
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2013-07-23T11:58:19Z
last_indexed 2018-02-09T04:35:36Z
id cronfa7438
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T12:00:43.7277049</datestamp><bib-version>v2</bib-version><id>7438</id><entry>2012-02-23</entry><title>Proofs, Programs, Processes</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><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-02-23</date><deptcode>SCS</deptcode><abstract>The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that realizers, although per-se untyped, can be assigned polymorphic recursive types and hence represent valid programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t.\ to the binary signed digit representation.</abstract><type>Journal Article</type><journal>Theory of Computing Systems</journal><volume>51</volume><journalNumber>3</journalNumber><paginationStart>313</paginationStart><paginationEnd>329</paginationEnd><publisher/><placeOfPublication/><issnPrint>1432-4350</issnPrint><issnElectronic>1433-0490</issnElectronic><keywords>program extraction, realizability, coinduction, verified programs, exact real number computation</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2012</publishedYear><publishedDate>2012-12-31</publishedDate><doi>10.1007/s00224-011-9325-8</doi><url/><notes></notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T12:00:43.7277049</lastEdited><Created>2012-02-23T17:01:55.0000000</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><orcid>0000-0002-2226-386X</orcid><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T12:00:43.7277049 v2 7438 2012-02-23 Proofs, Programs, Processes 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 2012-02-23 SCS The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that realizers, although per-se untyped, can be assigned polymorphic recursive types and hence represent valid programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t.\ to the binary signed digit representation. Journal Article Theory of Computing Systems 51 3 313 329 1432-4350 1433-0490 program extraction, realizability, coinduction, verified programs, exact real number computation 31 12 2012 2012-12-31 10.1007/s00224-011-9325-8 COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2013-10-17T12:00:43.7277049 2012-02-23T17:01:55.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Monika Seisenberger 0000-0002-2226-386X 2
title Proofs, Programs, Processes
spellingShingle Proofs, Programs, Processes
Ulrich Berger
Monika Seisenberger
title_short Proofs, Programs, Processes
title_full Proofs, Programs, Processes
title_fullStr Proofs, Programs, Processes
title_full_unstemmed Proofs, Programs, Processes
title_sort Proofs, Programs, Processes
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
d035399b2b324a63fe472ce0344653e0
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger
author Ulrich Berger
Monika Seisenberger
author2 Ulrich Berger
Monika Seisenberger
format Journal article
container_title Theory of Computing Systems
container_volume 51
container_issue 3
container_start_page 313
publishDate 2012
institution Swansea University
issn 1432-4350
1433-0490
doi_str_mv 10.1007/s00224-011-9325-8
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
document_store_str 0
active_str 0
description The objective of this paper is to provide a theoretical foundation for program extraction from proofs. We give a realizability interpretation for first-order proofs involving inductive and coinductive definitions and discuss its application to the synthesis of provably correct programs. We show that realizers, although per-se untyped, can be assigned polymorphic recursive types and hence represent valid programs in a lazy functional programming language such as Haskell. Programs extracted from proofs using coinduction can be understood as perpetual processes producing infinite streams of data. Typical applications of such processes are computations in exact real arithmetic. As an example we show how to extract a program computing the average of two real numbers w.r.t.\ to the binary signed digit representation.
published_date 2012-12-31T03:09:14Z
_version_ 1763749873181523968
score 11.037275

Similar Items