Document Open Access Logo

Extracting Non-Deterministic Concurrent Programs

Author Ulrich Berger

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.26.pdf
  • Filesize: 478 kB
  • 21 pages

Document Identifiers

Author Details

Ulrich Berger

Cite As Get BibTex

Ulrich Berger. Extracting Non-Deterministic Concurrent Programs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 26:1-26:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.26

Abstract

We introduce an extension of intuitionistic fixed point logic by a modal operator facilitating the extraction of non-deterministic concurrent programs from proofs. We apply this extension to program extraction in computable analysis, more precisely, to computing with Tsuiki's infinite Gray code for real numbers.

Subject Classification

Keywords
  • Proof theory
  • realizability
  • program extraction
  • non-determinism
  • concurrency
  • computable analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. U. Berger. Realisability for induction and coinduction with applications to constructive analysis. Jour. Universal Comput. Sci., 16(18):2535-2555, 2010. Google Scholar
  2. U. Berger and T. Hou. A realizability interpretation of Church’s simple theory of types. Mathematical Structures in Computer Science, 2016. To appear. Google Scholar
  3. U. Berger, K. Miyamoto, H. Schwichtenberg, and M. Seisenberger. Minlog - a tool for program extraction for supporting algebra and coalgebra. In CALCO-Tools, volume 6859 of LNCS, pages 393-399. Springer Verlag, Berlin, Heidelberg, New York, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22944-2_29.
  4. U. Berger, K. Miyamoto, H. Schwichtenberg, and H. Tsuiki. Logic for Gray-code computation. In Concepts of Proof in Mathematics, Philosophy, and Computer Science, Ontos Mathematical Logic 6. de Gruyter, 2016. To appear. Google Scholar
  5. S. Berghofer. Program Extraction in simply-typed Higher Order Logic. In Types for Proofs and Programs (TYPES'02), volume 2646 of LNCS, pages 21-38. Springer Verlag, Berlin, Heidelberg, New York, 2003. Google Scholar
  6. A. Bucciarelli, T. Ehrhard, and G. Manzonetto. A relational semantics for parallelism and non-determinism in a functional setting. Annals of Pure and Applied Logic, 163(7):918-934, 2012. Google Scholar
  7. C. M. Chuang. Extraction of Programs for Exact Real Number Computation Using Agda. PhD thesis, Swansea University, 2011. Google Scholar
  8. R.L. Constable. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, New Jersey, 1986. Google Scholar
  9. S. Hayashi and H. Nakano. PX: A Computational Logic. MIT Press, 1988. Google Scholar
  10. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1):55-92, 1991. Google Scholar
  11. C.-H.L. Ong. Non-determinism in a functional setting. In Proc. of LICS'93, pages 275-286, 1993. Google Scholar
  12. C. Paulin-Mohring. Inductive definitions in the system Coq; rules and properties. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, pages 328-345. LNCS Vol. 664, 1993. Google Scholar
  13. G.D. Plotkin. A powerdomain construction. SIAM J. Comput., 5(3):452-487, 1976. Google Scholar
  14. H. Tsuiki. Real Number Computation through Gray Code Embedding. Theoretical Computer Science, 284(2):467-485, 2002. Google Scholar
  15. G. Winskel. The Formal Semantics of Programming Languages. Foundations of Computing Series. The MIT Press, Cambridge, Massachusetts, 1993. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact