Document Open Access Logo

Extracting Imperative Programs from Proofs: In-place Quicksort

Authors Ulrich Berger, Monika Seisenberger, Gregory J. M. Woods

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2013.84.pdf
  • Filesize: 0.54 MB
  • 23 pages

Document Identifiers

Author Details

Ulrich Berger
Monika Seisenberger
Gregory J. M. Woods

Cite AsGet BibTex

Ulrich Berger, Monika Seisenberger, and Gregory J. M. Woods. Extracting Imperative Programs from Proofs: In-place Quicksort. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 84-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.TYPES.2013.84

Abstract

The process of program extraction is primarily associated with functional programs with less focus on imperative program extraction. In this paper we consider a standard problem for imperative programming: In-place Quicksort. We formalize a proof that every array of natural numbers can be sorted and apply a realizability interpretation to extract a program from the proof. Using monads we are able to exhibit the inherent imperative nature of the extracted program. We see this as a first step towards an automated extraction of imperative programs. The case study is carried out in the interactive proof assistant Minlog.
Keywords
  • Program Extraction
  • Verification
  • Realizability
  • Imperative Programs
  • In-Place Quicksort,Computational Monads
  • Minlog

Metrics

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

References

  1. J. R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edition, 2010. Google Scholar
  2. Agda. URL: http://wiki.portal.chalmers.se/agda/.
  3. H. Benl, U. Berger, H. Schwichtenberg, M. Seisenberger, and W. Zuber. Proof theory at work: Program development in the Minlog system. In Automated Deduction, volume II of Applied Logic Series, pages 41-71. Kluwer, 1998. Google Scholar
  4. U. Berger, K. Miyamoto, H. Schwichtenberg, and M. Seisenberger. Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras. In A. Corradini, B. Klin, and C. Cîrstea, editors, CALCO 2011, volume 6859 of Lecture Notes in Computer Science, pages 393-399. Springer, 2011. Google Scholar
  5. U. Berger and M. Seisenberger. Proofs, Programs, Processes. Theory of Computing Systems, 51(3):313-329, 2012. Google Scholar
  6. S. Berghofer. Program extraction in simply-typed higher order logic. In H. Geuvers and F. Wiedijk, editors, TYPES 2002, volume 2646 of Lecture Notes in Computer Science, pages 21-38. Springer, 2003. Google Scholar
  7. B. Brock, M. Kaufmann, and J. S. Moore. ACL2 Theorems about Commercial Microprocessors. In Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 275-293. Springer-Verlag, 1996. Google Scholar
  8. C. M. Chuang. Extraction of Programs for Exact Real Number Computation Using Agda. PhD thesis, Swansea University, Wales, 2011. Google Scholar
  9. The Coq Proof Assistant. URL: http://coq.inria.fr/.
  10. M. Erwig and D. Ren. Monadification of Functional Programs. Science of Computer Programming, 52(1-3):101-129, 2004. Google Scholar
  11. S. Hallerstede and M. Leuschel. Experiments in program verification using Event-B. Formal Aspects of Computing, 24:97-125, 2012. Google Scholar
  12. C. A. R. Hoare. Quicksort. The Computer Journal, 5(1):10-16, 1962. Google Scholar
  13. Isabelle. URL: http://isabelle.in.tum.de/.
  14. S. C. Kleene. On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic, 10:109-124, 1945. Google Scholar
  15. G. Kreisel. Interpretation of Analysis by means of Constructive Functionals of Finite Types. Constructivity in Mathematics, pages 101-128, 1959. Google Scholar
  16. J. Krivine. Realizability Algebras: A Program to Well Order ℝ. Logical Methods in Computer Science, 7:1-47, 2011. Google Scholar
  17. P. Letouzey. A New Extraction for Coq. In Types for Proofs and Programs, TYPES 2002, volume 2646 of Lecture Notes in Computer Science, pages 200-219, 2003. Google Scholar
  18. The Minlog System. URL: http://www.minlog-system.de.
  19. A. Miquel. Classical Program Extraction in the Calculus of Constructions. In CSL 2007, volume 4646 of Lecture Notes in Computer Science, pages 313-327, 2007. Google Scholar
  20. K. Miyamoto, F. Nordvall Forsberg, and H. Schwichtenberg. Program Extraction from Nested Definitions. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, ITP 2013, volume 7998 of Lecture Notes in Computer Science, pages 370 - 385. Springer, 2013. Google Scholar
  21. E. Moggi. Notions of Computation and Monads. Information and Computation, 93(1):55-92, 1991. Google Scholar
  22. PRL Project. URL: http://www.nuprl.org/.
  23. I. Poernomo, J. N. Crossley, and M. Wirsing. Adapting Proofs-as-Programs: The Curry-Howard Protocol. Springer, 2005. Google Scholar
  24. Swansea Minlog Repository. URL: http://cs.swan.ac.uk/minlog/.
  25. D. Ratiu and T. Trifonov. Exploring the Computational Content of the Infinite Pigeonhole Principle. Journal of Logic and Computation, 22(2):329-350, 2012. Google Scholar
  26. S. Ray and R. Sumners. Verification of an In-place Quicksort in ACL2. In D. Borrione, M. Kaufmann, and J. S. Moore, editors, 3rd International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2002), pages 204-212, Grenoble, 2002. Google Scholar
  27. H. Schwichtenberg and S. S. Wainer. Proofs and Computations. Perspectives in Logic. Assoc. Symb. Logic and Cambridge Univ. Press, 2012. Google Scholar
  28. TIOBE. URL: http://www.tiobe.com/index.php/content/paperinfo/tpci/index.html.
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 Imprint Privacy Contact