Extracting total Amb programs from proofs
From MaRDI portal
Publication:6166786
DOI10.1007/978-3-030-99336-8_4zbMath1528.68077arXiv2307.12454MaRDI QIDQ6166786
Publication date: 3 August 2023
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2307.12454
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proofs, programs, processes
- A semantics for concurrent separation logic
- Resources, concurrency, and local reasoning
- A theory for nondeterminism, parallelism, communication, and concurrency
- A fundamental effect in computations on real numbers
- Proofs as processes
- PCF extended with real numbers
- Real number computation through Gray code embedding.
- Optimized program extraction for induction and coinduction
- On the representation of McCarthy's \(amb\) in the \(\pi\)-calculus
- Real number computation with committed choice logic programming languages
- Erratic Fudgets: A semantic theory for an embedded coordination language
- An abstract data type for real numbers
- \textsc{Prawf}: an interactive proof system for program extraction
- Intuitionistic fixed point logic
- Fifty years of Hoare's logic
- Propositions as sessions
- Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
- From coinductive proofs to exact real arithmetic: theory and applications
- Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras
- Proofs and Computations
- A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Continuous Lattices and Domains
- Computing with continuous objects: a uniform co-inductive approach
- Amb Breaks Well-Pointedness, Ground Amb Doesn't
- Extracting Non-Deterministic Concurrent Programs.
- On asynchronous eventful session semantics
- Linear logic propositions as session types
- Concurrent Gaussian Elimination
This page was built for publication: Extracting total Amb programs from proofs
