Conference Paper/Proceeding/Abstract 1258 views 116 downloads
Extracting nondeterministic concurrent programs
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)., Volume: 62, Pages: 26:1 - 26:21
Swansea University Author:
Ulrich Berger
-
PDF | Version of Record
Released under the terms of a Creative Commons Attribution 3.0 Unported license (CC-BY).
Download (529.93KB)
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...
| 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 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| 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. |
|---|---|
| Keywords: |
Proof theory, realizability, program extraction, nondeterminism, concurrency, computable analysis |
| College: |
Faculty of Science and Engineering |
| Start Page: |
26:1 |
| End Page: |
26:21 |