No Cover Image

Conference Paper/Proceeding/Abstract 510 views 38 downloads

Extracting nondeterministic concurrent programs / Ulrich, Berger

Computer Science Logic 2016, Volume: 62, Pages: 26:1 - 26:21

Swansea University Author: Ulrich, Berger

  • 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)

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: Computer Science Logic 2016
ISBN: 978-3-95977-022-4
ISSN: 1868-8969
Published: 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
Start Page: 26:1
End Page: 26:21