No Cover Image

Conference Paper/Proceeding/Abstract 740 views 71 downloads

Extracting total Amb programs from proofs

Ulrich Berger Orcid Logo, Hideki Tsuiki Orcid Logo

Programming Languages and Systems, Volume: 13240, Pages: 85 - 113

Swansea University Author: Ulrich Berger Orcid Logo

  • 60606.pdf

    PDF | Version of Record

    This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License

    Download (666.47KB)

Check full text

DOI (Published version): 10.1007/978-3-030-99336-8_4

Abstract

We present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators,...

Full description

Published in: Programming Languages and Systems
ISBN: 9783030993351 9783030993368
ISSN: 0302-9743 1611-3349
Published: Cham Springer International Publishing 2022
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa60606
first_indexed 2022-07-22T21:21:44Z
last_indexed 2023-01-13T19:20:51Z
id cronfa60606
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2022-10-31T14:59:52.7779300</datestamp><bib-version>v2</bib-version><id>60606</id><entry>2022-07-22</entry><title>Extracting total Amb programs from proofs</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>2022-07-22</date><deptcode>MACS</deptcode><abstract>We present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators, $B_{A}$ (restriction, a strengthening of implication) and $\downdownarrows(B)$ (total concurrency). The source of the extraction are formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Programming Languages and Systems</journal><volume>13240</volume><journalNumber/><paginationStart>85</paginationStart><paginationEnd>113</paginationEnd><publisher>Springer International Publishing</publisher><placeOfPublication>Cham</placeOfPublication><isbnPrint>9783030993351</isbnPrint><isbnElectronic>9783030993368</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords>logic, proof theory, program extraction, realisability, concurrency, nondeterminism, exact real number computation</keywords><publishedDay>29</publishedDay><publishedMonth>3</publishedMonth><publishedYear>2022</publishedYear><publishedDate>2022-03-29</publishedDate><doi>10.1007/978-3-030-99336-8_4</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>This work was supported by IRSES Nr. 612638 CORCON and Nr. 294962 COMPUTAL of the European Commission, the JSPS Core-toCore Program, A. Advanced research Networks and JSPS KAKENHI 15K00015 as well as the Marie Curie RISE project CID (H2020-MSCA-RISE-2016-731143).</funders><projectreference/><lastEdited>2022-10-31T14:59:52.7779300</lastEdited><Created>2022-07-22T21:15:36.4630888</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>Hideki</firstname><surname>Tsuiki</surname><orcid>0000-0003-0854-948x</orcid><order>2</order></author></authors><documents><document><filename>60606__24926__4ecd73688bd84d28a799d80efdfd087a.pdf</filename><originalFilename>60606.pdf</originalFilename><uploaded>2022-08-15T14:59:11.0357558</uploaded><type>Output</type><contentLength>682463</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>http://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2022-10-31T14:59:52.7779300 v2 60606 2022-07-22 Extracting total Amb programs from proofs 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2022-07-22 MACS We present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators, $B_{A}$ (restriction, a strengthening of implication) and $\downdownarrows(B)$ (total concurrency). The source of the extraction are formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb. Conference Paper/Proceeding/Abstract Programming Languages and Systems 13240 85 113 Springer International Publishing Cham 9783030993351 9783030993368 0302-9743 1611-3349 logic, proof theory, program extraction, realisability, concurrency, nondeterminism, exact real number computation 29 3 2022 2022-03-29 10.1007/978-3-030-99336-8_4 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Not Required This work was supported by IRSES Nr. 612638 CORCON and Nr. 294962 COMPUTAL of the European Commission, the JSPS Core-toCore Program, A. Advanced research Networks and JSPS KAKENHI 15K00015 as well as the Marie Curie RISE project CID (H2020-MSCA-RISE-2016-731143). 2022-10-31T14:59:52.7779300 2022-07-22T21:15:36.4630888 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 Hideki Tsuiki 0000-0003-0854-948x 2 60606__24926__4ecd73688bd84d28a799d80efdfd087a.pdf 60606.pdf 2022-08-15T14:59:11.0357558 Output 682463 application/pdf Version of Record true This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License true eng http://creativecommons.org/licenses/by/4.0/
title Extracting total Amb programs from proofs
spellingShingle Extracting total Amb programs from proofs
Ulrich Berger
title_short Extracting total Amb programs from proofs
title_full Extracting total Amb programs from proofs
title_fullStr Extracting total Amb programs from proofs
title_full_unstemmed Extracting total Amb programs from proofs
title_sort Extracting total Amb programs from proofs
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
Hideki Tsuiki
format Conference Paper/Proceeding/Abstract
container_title Programming Languages and Systems
container_volume 13240
container_start_page 85
publishDate 2022
institution Swansea University
isbn 9783030993351
9783030993368
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-030-99336-8_4
publisher Springer International Publishing
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 present a logical system CFP (Concurrent Fixed Point Logic) that supports the extraction of nondeterministic and concurrent programs that are provably total and correct. CFP is an intuitionistic first-order logic with inductive and coinductive definitions extended by two propositional operators, $B_{A}$ (restriction, a strengthening of implication) and $\downdownarrows(B)$ (total concurrency). The source of the extraction are formal CFP proofs, the target is a lambda calculus with constructors and recursion extended by a constructor Amb (for McCarthy's amb) which is interpreted operationally as globally angelic choice and is used to implement nondeterminism and concurrency. The correctness of extracted programs is proven via an intermediate domain-theoretic denotational semantics. We demonstrate the usefulness of our system by extracting a nondeterministic program that translates infinite Gray code into the signed digit representation. A noteworthy feature of our system is that the proof rules for restriction and concurrency involve variants of the classical law of excluded middle that would not be interpretable computationally without Amb.
published_date 2022-03-29T20:13:34Z
_version_ 1821347166783799296
score 11.04748

Similar Items