No Cover Image

Book 1509 views

Realisability and adequacy for (co)induction

Ulrich Berger, David Benton, David Benton, David Benton, Katharina Hall, Robert Rhys

Pages: 49 - 60

Swansea University Author: Ulrich Berger

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

DOI (Published version): 10.4230/OASIcs.CCA.2009.2258

Abstract

We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped $\lambda$-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the...

Full description

Published: Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2009
Online Access: http://drops.dagstuhl.de/opus/volltexte/2009/2258
URI: https://cronfa.swan.ac.uk/Record/cronfa53
first_indexed 2013-07-23T11:49:23Z
last_indexed 2018-02-09T04:27:21Z
id cronfa53
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2013-10-17T11:56:18.4177127</datestamp><bib-version>v2</bib-version><id>53</id><entry>2012-02-23</entry><title>Realisability and adequacy for (co)induction</title><swanseaauthors><author><sid>61199ae25042a5e629c5398c4a40a4f5</sid><firstname>Ulrich</firstname><surname>Berger</surname><name>Ulrich Berger</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-02-23</date><abstract>We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped $\lambda$-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis.</abstract><type>Book</type><journal></journal><volume></volume><journalNumber></journalNumber><paginationStart>49</paginationStart><paginationEnd>60</paginationEnd><publisher>Schloss Dagstuhl - Leibniz-Zentrum f&#xFC;r Informatik</publisher><placeOfPublication/><issnPrint/><issnElectronic/><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2009</publishedYear><publishedDate>2009-12-31</publishedDate><doi>10.4230/OASIcs.CCA.2009.2258</doi><url>http://drops.dagstuhl.de/opus/volltexte/2009/2258</url><notes>In CCA '09, Proc. Sixth Intl. Conference on Computability and Complexity in Analysis, Ljubljana, Slovenia</notes><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><apcterm/><lastEdited>2013-10-17T11:56:18.4177127</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><order>1</order></author><author><firstname>David</firstname><surname>Benton</surname><order>2</order></author><author><firstname>David</firstname><surname>Benton</surname><order>3</order></author><author><firstname>David</firstname><surname>Benton</surname><order>4</order></author><author><firstname>Katharina</firstname><surname>Hall</surname><order>5</order></author><author><firstname>Robert</firstname><surname>Rhys</surname><order>6</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2013-10-17T11:56:18.4177127 v2 53 2012-02-23 Realisability and adequacy for (co)induction 61199ae25042a5e629c5398c4a40a4f5 Ulrich Berger Ulrich Berger true false 2012-02-23 We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped $\lambda$-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis. Book 49 60 Schloss Dagstuhl - Leibniz-Zentrum für Informatik 31 12 2009 2009-12-31 10.4230/OASIcs.CCA.2009.2258 http://drops.dagstuhl.de/opus/volltexte/2009/2258 In CCA '09, Proc. Sixth Intl. Conference on Computability and Complexity in Analysis, Ljubljana, Slovenia COLLEGE NANME COLLEGE CODE Swansea University 2013-10-17T11:56:18.4177127 2012-02-23T17:01:55.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 1 David Benton 2 David Benton 3 David Benton 4 Katharina Hall 5 Robert Rhys 6
title Realisability and adequacy for (co)induction
spellingShingle Realisability and adequacy for (co)induction
Ulrich Berger
title_short Realisability and adequacy for (co)induction
title_full Realisability and adequacy for (co)induction
title_fullStr Realisability and adequacy for (co)induction
title_full_unstemmed Realisability and adequacy for (co)induction
title_sort Realisability and adequacy for (co)induction
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
David Benton
David Benton
David Benton
Katharina Hall
Robert Rhys
format Book
container_start_page 49
publishDate 2009
institution Swansea University
doi_str_mv 10.4230/OASIcs.CCA.2009.2258
publisher Schloss Dagstuhl - Leibniz-Zentrum für Informatik
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/2009/2258
document_store_str 0
active_str 0
description We prove the correctness of a formalised realisability interpretation of extensions of first-order theories by inductive and coinductive definitions in an untyped $\lambda$-calculus with fixed-points. We illustrate the use of this interpretation for program extraction by some simple examples in the area of exact real number computation and hint at further non-trivial applications in computable analysis.
published_date 2009-12-31T03:03:06Z
_version_ 1851451125675327488
score 11.089572

Similar Items