No Cover Image

Conference Paper/Proceeding/Abstract 559 views 38 downloads

Extracting total Amb programs from proofs

Ulrich Berger Orcid Logo, Hideki Tsuiki Orcid Logo

Programming Languages and Systems, Volume: 13240, Pages: 85 - 113

Swansea University Author: Ulrich Berger Orcid Logo

  • 60606.pdf

    PDF | Version of Record

    This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License

    Download (666.47KB)

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,...

Full description

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
Tags: Add Tag
No Tags, Be the first to tag this record!
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