No Cover Image

Book chapter 1557 views

Proofs, Programs, Processes

Ulrich Berger Orcid Logo, Monika Seisenberger

Programs, Proofs, Processes, Volume: 6158, Pages: 39 - 48

Swansea University Author: Ulrich Berger Orcid Logo

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

Check full text

DOI (Published version): 10.1007/978-3-642-13962-8_5

Abstract

<p>We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to programs in a lazy functional programming lan...

Full description

Published in: Programs, Proofs, Processes
ISSN: 0302-9743 1611-3349
Published: Berlin Springer 2010
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa5273
first_indexed 2013-07-23T11:52:09Z
last_indexed 2018-02-09T04:31:26Z
id cronfa5273
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T11:59:55.7024233</datestamp><bib-version>v2</bib-version><id>5273</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></swanseaauthors><date>2012-02-23</date><deptcode>MACS</deptcode><abstract>&lt;p&gt;We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to 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 with respect to the binary signed digit representation.&lt;/p&gt;</abstract><type>Book chapter</type><journal>Programs, Proofs, Processes</journal><volume>6158</volume><journalNumber></journalNumber><paginationStart>39</paginationStart><paginationEnd>48</paginationEnd><publisher>Springer</publisher><placeOfPublication>Berlin</placeOfPublication><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2010</publishedYear><publishedDate>2010-12-31</publishedDate><doi>10.1007/978-3-642-13962-8_5</doi><url>http://www.springerlink.com/content/g81ktw31q3683602/</url><notes>Lecture Notes in Computer Science Volume 6158</notes><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T11:59:55.7024233</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><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T11:59:55.7024233 v2 5273 2012-02-23 Proofs, Programs, Processes 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2012-02-23 MACS <p>We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to 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 with respect to the binary signed digit representation.</p> Book chapter Programs, Proofs, Processes 6158 39 48 Springer Berlin 0302-9743 1611-3349 31 12 2010 2010-12-31 10.1007/978-3-642-13962-8_5 http://www.springerlink.com/content/g81ktw31q3683602/ Lecture Notes in Computer Science Volume 6158 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2013-10-17T11:59:55.7024233 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 2
title Proofs, Programs, Processes
spellingShingle Proofs, Programs, Processes
Ulrich Berger
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
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
Monika Seisenberger
format Book chapter
container_title Programs, Proofs, Processes
container_volume 6158
container_start_page 39
publishDate 2010
institution Swansea University
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-642-13962-8_5
publisher Springer
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://www.springerlink.com/content/g81ktw31q3683602/
document_store_str 0
active_str 0
description <p>We study a realisability interpretation for inductive and coinductive definitions and discuss its application to program extraction from proofs. A speciality of this interpretation is that realisers are given by terms that correspond directly to 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 with respect to the binary signed digit representation.</p>
published_date 2010-12-31T18:09:55Z
_version_ 1821339387306180608
score 11.04748

Similar Items