Conference Paper/Proceeding/Abstract 740 views 71 downloads
Extracting total Amb programs from proofs
,
Hideki Tsuiki
Programming Languages and Systems, Volume: 13240, Pages: 85 - 113
Swansea University Author:
Ulrich Berger
-
PDF | Version of Record
This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License
Download (666.47KB)
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,...
| 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 |
| 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. |
|---|---|
| Keywords: |
logic, proof theory, program extraction, realisability, concurrency, nondeterminism, exact real number computation |
| College: |
Faculty of Science and Engineering |
| 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). |
| Start Page: |
85 |
| End Page: |
113 |