No Cover Image

Journal article 86 views 7 downloads

Constructive Domains with Classical Witnesses

Dirk Pattinson, Mina Cyrus Orcid Logo

Logical Methods in Computer Science, Volume: 17, Issue: 1, Pages: 19:1 - 19:30

Swansea University Author: Mina Cyrus Orcid Logo

  • 68135.VOR.pdf

    PDF | Version of Record

    © D. Pattinson and M. Mohammadian. This work is licensed under the Creative Commons Attribution License.

    Download (468.3KB)

Check full text

DOI (Published version): 10.23638/LMCS-17(1:19)2021

Abstract

We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain ba...

Full description

Published in: Logical Methods in Computer Science
ISSN: 1860-5974
Published: Logical Methods in Computer Science e.V. 2021
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa68135
first_indexed 2025-01-09T20:32:44Z
last_indexed 2025-02-14T05:44:38Z
id cronfa68135
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-02-13T11:48:09.8809873</datestamp><bib-version>v2</bib-version><id>68135</id><entry>2024-11-01</entry><title>Constructive Domains with Classical Witnesses</title><swanseaauthors><author><sid>fb5320369ba356b005c93d6e38c94caf</sid><ORCID>0009-0005-9085-4652</ORCID><firstname>Mina</firstname><surname>Cyrus</surname><name>Mina Cyrus</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-11-01</date><deptcode>MACS</deptcode><abstract>We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions.</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>17</volume><journalNumber>1</journalNumber><paginationStart>19:1</paginationStart><paginationEnd>19:30</paginationEnd><publisher>Logical Methods in Computer Science e.V.</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic>1860-5974</issnElectronic><keywords>Domain Theory, Constructive Mathematics, Real Number Computation, Predomain Base, Function Spaces</keywords><publishedDay>2</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2021</publishedYear><publishedDate>2021-03-02</publishedDate><doi>10.23638/LMCS-17(1:19)2021</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm>Not Required</apcterm><funders/><projectreference/><lastEdited>2025-02-13T11:48:09.8809873</lastEdited><Created>2024-11-01T11:08:29.4826098</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>Dirk</firstname><surname>Pattinson</surname><order>1</order></author><author><firstname>Mina</firstname><surname>Cyrus</surname><orcid>0009-0005-9085-4652</orcid><order>2</order></author></authors><documents><document><filename>68135__33250__6b92968352ed4075bfd6d51644c1812f.pdf</filename><originalFilename>68135.VOR.pdf</originalFilename><uploaded>2025-01-06T11:38:46.2015052</uploaded><type>Output</type><contentLength>479535</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; D. Pattinson and M. Mohammadian. This work is licensed under the Creative Commons Attribution License.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0</licence></document></documents><OutputDurs/></rfc1807>
spelling 2025-02-13T11:48:09.8809873 v2 68135 2024-11-01 Constructive Domains with Classical Witnesses fb5320369ba356b005c93d6e38c94caf 0009-0005-9085-4652 Mina Cyrus Mina Cyrus true false 2024-11-01 MACS We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions. Journal Article Logical Methods in Computer Science 17 1 19:1 19:30 Logical Methods in Computer Science e.V. 1860-5974 Domain Theory, Constructive Mathematics, Real Number Computation, Predomain Base, Function Spaces 2 3 2021 2021-03-02 10.23638/LMCS-17(1:19)2021 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Not Required 2025-02-13T11:48:09.8809873 2024-11-01T11:08:29.4826098 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Dirk Pattinson 1 Mina Cyrus 0009-0005-9085-4652 2 68135__33250__6b92968352ed4075bfd6d51644c1812f.pdf 68135.VOR.pdf 2025-01-06T11:38:46.2015052 Output 479535 application/pdf Version of Record true © D. Pattinson and M. Mohammadian. This work is licensed under the Creative Commons Attribution License. true eng https://creativecommons.org/licenses/by/4.0
title Constructive Domains with Classical Witnesses
spellingShingle Constructive Domains with Classical Witnesses
Mina Cyrus
title_short Constructive Domains with Classical Witnesses
title_full Constructive Domains with Classical Witnesses
title_fullStr Constructive Domains with Classical Witnesses
title_full_unstemmed Constructive Domains with Classical Witnesses
title_sort Constructive Domains with Classical Witnesses
author_id_str_mv fb5320369ba356b005c93d6e38c94caf
author_id_fullname_str_mv fb5320369ba356b005c93d6e38c94caf_***_Mina Cyrus
author Mina Cyrus
author2 Dirk Pattinson
Mina Cyrus
format Journal article
container_title Logical Methods in Computer Science
container_volume 17
container_issue 1
container_start_page 19:1
publishDate 2021
institution Swansea University
issn 1860-5974
doi_str_mv 10.23638/LMCS-17(1:19)2021
publisher Logical Methods in Computer Science e.V.
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 1
active_str 0
description We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness assertions classically. Technically, we start from a predomain base and construct a completion. We then investigate continuity with respect to the Scott topology, and present a construction of the function space. We then discuss our main motivating example in detail, and instantiate our theory to real numbers that we conceptualise as the total elements of the completion of the predomain of rational intervals, and prove a representation theorem that precisely delineates the class of representable continuous functions.
published_date 2021-03-02T06:17:38Z
_version_ 1830350496803586048
score 11.317152

Similar Items