No Cover Image

Conference Paper/Proceeding/Abstract 1259 views 116 downloads

Extracting nondeterministic concurrent programs

Ulrich Berger Orcid Logo

25th EACSL Annual Conference on Computer Science Logic (CSL 2016)., Volume: 62, Pages: 26:1 - 26:21

Swansea University Author: Ulrich Berger Orcid Logo

  • berger-csl16-revised.pdf

    PDF | Version of Record

    Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY).

    Download (529.93KB)

Check full text

DOI (Published version): 10.4230/LIPIcs.CSL.2016.26

Abstract

We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of nondeterministic concurrent programsfrom proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code f...

Full description

Published in: 25th EACSL Annual Conference on Computer Science Logic (CSL 2016).
ISBN: 978-3-95977-022-4
ISSN: 1868-8969
Published: Dagstuhl, Germany Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik 2016
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa28974
first_indexed 2016-10-13T18:53:46Z
last_indexed 2021-01-29T03:45:56Z
id cronfa28974
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2021-01-28T16:08:04.3671501</datestamp><bib-version>v2</bib-version><id>28974</id><entry>2016-06-21</entry><title>Extracting nondeterministic concurrent programs</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>2016-06-21</date><deptcode>MACS</deptcode><abstract>We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of nondeterministic concurrent programsfrom proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>25th EACSL Annual Conference on Computer Science Logic (CSL 2016).</journal><volume>62</volume><journalNumber/><paginationStart>26:1</paginationStart><paginationEnd>26:21</paginationEnd><publisher>Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik</publisher><placeOfPublication>Dagstuhl, Germany</placeOfPublication><isbnPrint/><isbnElectronic>978-3-95977-022-4</isbnElectronic><issnPrint/><issnElectronic>1868-8969</issnElectronic><keywords>Proof theory, realizability, program extraction, nondeterminism, concurrency, computable analysis</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2016</publishedYear><publishedDate>2016-12-31</publishedDate><doi>10.4230/LIPIcs.CSL.2016.26</doi><url>https://drops.dagstuhl.de/opus/volltexte/2016/6566/pdf/LIPIcs-CSL-2016-26.pdf</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/><lastEdited>2021-01-28T16:08:04.3671501</lastEdited><Created>2016-06-21T14:26:36.1215742</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></authors><documents><document><filename>0028974-22072016154920.pdf</filename><originalFilename>berger-csl16-revised.pdf</originalFilename><uploaded>2016-07-22T15:49:20.3270000</uploaded><type>Output</type><contentLength>489826</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY).</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/3.0/legalcode</licence></document></documents><OutputDurs/></rfc1807>
spelling 2021-01-28T16:08:04.3671501 v2 28974 2016-06-21 Extracting nondeterministic concurrent programs 61199ae25042a5e629c5398c4a40a4f5 0000-0002-7677-3582 Ulrich Berger Ulrich Berger true false 2016-06-21 MACS We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of nondeterministic concurrent programsfrom proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers. Conference Paper/Proceeding/Abstract 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). 62 26:1 26:21 Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik Dagstuhl, Germany 978-3-95977-022-4 1868-8969 Proof theory, realizability, program extraction, nondeterminism, concurrency, computable analysis 31 12 2016 2016-12-31 10.4230/LIPIcs.CSL.2016.26 https://drops.dagstuhl.de/opus/volltexte/2016/6566/pdf/LIPIcs-CSL-2016-26.pdf COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2021-01-28T16:08:04.3671501 2016-06-21T14:26:36.1215742 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Ulrich Berger 0000-0002-7677-3582 1 0028974-22072016154920.pdf berger-csl16-revised.pdf 2016-07-22T15:49:20.3270000 Output 489826 application/pdf Version of Record true Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY). true eng https://creativecommons.org/licenses/by/3.0/legalcode
title Extracting nondeterministic concurrent programs
spellingShingle Extracting nondeterministic concurrent programs
Ulrich Berger
title_short Extracting nondeterministic concurrent programs
title_full Extracting nondeterministic concurrent programs
title_fullStr Extracting nondeterministic concurrent programs
title_full_unstemmed Extracting nondeterministic concurrent programs
title_sort Extracting nondeterministic concurrent programs
author_id_str_mv 61199ae25042a5e629c5398c4a40a4f5
author_id_fullname_str_mv 61199ae25042a5e629c5398c4a40a4f5_***_Ulrich Berger
author Ulrich Berger
author2 Ulrich Berger
format Conference Paper/Proceeding/Abstract
container_title 25th EACSL Annual Conference on Computer Science Logic (CSL 2016).
container_volume 62
container_start_page 26:1
publishDate 2016
institution Swansea University
isbn 978-3-95977-022-4
issn 1868-8969
doi_str_mv 10.4230/LIPIcs.CSL.2016.26
publisher Schloss Dagstuhl-Leibniz-Zentrum fuer 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 https://drops.dagstuhl.de/opus/volltexte/2016/6566/pdf/LIPIcs-CSL-2016-26.pdf
document_store_str 1
active_str 0
description We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of nondeterministic concurrent programsfrom proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.
published_date 2016-12-31T13:00:50Z
_version_ 1821319941476843520
score 11.048042

Similar Items