Abstract
One can argue that writing proofs might be better than writing programs, for the following simple reason: There is no algorithm that can check whether a program meets its specification, but it is easy to check whether a given proof is correct.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Joseph L. Bates and Robert L. Constable. Proofs as programs.ACM Transactions on Programming Languages and Systems7(1):113–136, January 1985.
Ulrich Berger and Helmut Schwichtenberg. Program extraction from classical proofs. In D. Leivant, editorLogic and Computational Complexity International Workshop LCC ‘84 Indianapolis IN USA October 1994 volume 960 of Lecture Notes in Computer Science pages 77–97. Springer Verlag, Berlin, Heidelberg, New York, 1995.
Ulrich Berger and Helmut Schwichtenberg. The greatest common divisor: a case study for program extraction from classical proofs. In S. Berardi and M. Coppo, editorsTypes for Proofs and Programs. International Workshop TYPES ‘85 Torino Italy June 199,5. Selected Papersvolume 1158 of Lecture Notes in Computer Sciencepages 36–46. Springer Verlag, Berlin, Heidelberg, New York, 1996.
Christopher Alan Goad.Computational uses of the manipulation of formal proofs.PhD thesis, Stanford University, August 1980. Stanford Department of Computer Science Report No. STAN-CS-80–819.
Helmut Schwichtenberg. Programmentwicklung durch Beweistransformation: Das Maximalsegmentproblem.Sitzungsber. d. Bayer. Akad. d. Wiss. Math.-Nat. Kl.pages 8*-12*, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Benl, H., Schwichtenberg, H. (1999). Formal Correctness Proofs of Functional Programs: Dijkstra’s Algorithm, a Case Study. In: Berger, U., Schwichtenberg, H. (eds) Computational Logic. NATO ASI Series, vol 165. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-58622-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-58622-4_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-63670-7
Online ISBN: 978-3-642-58622-4
eBook Packages: Springer Book Archive