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 As Get 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.

Subject Classification

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 About DROPS Imprint Privacy Contact