No Cover Image

Conference Paper/Proceeding/Abstract 414 views 32 downloads

Extracting nondeterministic concurrent programs / Ulrich, Berger

Computer Science Logic 2016

Swansea University Author: Ulrich, Berger

  • berger-csl16-revised.pdf

    PDF | Version of Record

    © Ulrich Berger; licensed under Creative Commons 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
College: College of Science