Extracting total Amb programs from proofs

DOI10.1007/978-3-030-99336-8_4MaRDI QIDQ6166786zbMATH OpenFDO

Authors Ulrich Berger, Hideki Tsuiki

Publication date 3 August 2023

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2307.12454

Mathematics Subject Classification ID

Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Recommendations

• Extracting non-deterministic concurrent programs
• \textsc{Prawf}: an interactive proof system for program extraction
• Proofs and programs: A naïve approach to program extraction
• Intuitionistic fixed point logic
• Extraction and verification of programs by analysis of formal proofs

Cites work

• \textsc{Prawf}: an interactive proof system for program extraction
• A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations
• A fundamental effect in computations on real numbers
• A semantics for concurrent separation logic
• A theory for nondeterminism, parallelism, communication, and concurrency
• Amb Breaks Well-Pointedness, Ground Amb Doesn't
• An abstract data type for real numbers
• Computing with continuous objects: a uniform co-inductive approach
• Concurrent Gaussian Elimination
• Continuous Lattices and Domains
• Erratic Fudgets: A semantic theory for an embedded coordination language
• Extracting non-deterministic concurrent programs
• Fifty years of Hoare's logic
• From coinductive proofs to exact real arithmetic: theory and applications
• scientific article; zbMATH DE number 3902001 (Why is no real title available?)
• scientific article; zbMATH DE number 1460545 (Why is no real title available?)
• scientific article; zbMATH DE number 1418339 (Why is no real title available?)
• scientific article; zbMATH DE number 3322506 (Why is no real title available?)
• Intuitionistic fixed point logic
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Linear logic propositions as session types
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Normal form simulation for McCarthy's \textsf{amb}
• On asynchronous eventful session semantics
• On the representation of McCarthy's amb in the -calculus
• Optimized program extraction for induction and coinduction
• PCF extended with real numbers
• Proofs and computations
• Proofs as processes
• Proofs, programs, processes
• Propositions as sessions
• Real number computation through Gray code embedding.
• Real number computation with committed choice logic programming languages
• Resources, concurrency, and local reasoning
• Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
• Types and programing languages

This page was built for publication: Extracting total Amb programs from proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6166786)