Abstract
There are two ways of reasoning about functional programs in the constructive type theory of the Nuprl proof development system. Nuprl can be used in a conventional program-verification mode, in which functional programs are written in a familiar style and then proven to be correct. It can also be used in an extraction mode, where programs are not written explicitly, but instead are extracted from mathematical proofs. Nuprl is the only constructive type theory to support both of these approaches. These approaches are illustrated by applying Nuprl to Boyer and Moore's “majority” algorithm.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. F. Allen. A non-type theoretic definition of Martin-Löfs types. In Proceedings of the Second Annual Symposium on Logic in Computer Science, pages 215–221. IEEE Computer Society, 1987.
S. F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987.
S. F. Allen, R. L. Constable, D. J. Howe, and W. B. Aitken. The semantics of reflected proof. In Proceedings of the Fifth Annual Symposium on Logic and Computer Science, pages 95–107. IEEE Computer Society, June 1990.
R. Backhouse. Algorithm development in Martin-Löf's type theory. Technical report, University of Essex, 1984.
D. A. Basin and P. Delvecchio. Verification of combinational logic in Nuprl. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, Ithaca, New York, 1989.
D. A. Basin and D. J. Howe. Some normalization properties of Martin-Löfs type theory, and applications. In T. Ito and A. Meyer, editors, Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, pages 475–494. Springer-Verlag, 1991.
R. Boyer and J. Moore. MJRTY, a fast majority vote algorithm. Technical report, University of Texas at Austin, 1981.
J. Chirimar and D. J. Howe. Implementing constructive real analysis: a preliminary report. In Symposium on Constructivity in Computer Science, Lecture Notes in Computer Science. Springer-Verlag, 1991. To appear.
R. Constable and D. Howe. Nuprl as a general logic. In P. Odifreddi, editor, Logic in Computer Science, pages 77–90. Academic Press, 1990.
R. Constable and S. Smith. Partial objects in constructive type theory. Proceedings of the Second Annual Symposium on Logic in Computer Science, pages 183–193, March 1987. (Cornell TR 87–822).
R. L. Constable and D. J. Howe. Implementing metamathematics as an approach to automatic theorem proving. In R. Banerji, editor, Formal Techniques in Artificial Intelligence: A Source Book, pages 45–76. Elsevier Science Publishers (North-Holland), 1990.
R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76:95–120, 1988.
S. Feferman. A language and axioms for explicit mathematics. In Dold, A. and B. Eckmann, editor, Algebra and Logic, volume 450 of Lecture Notes in Mathematics, pages 87–139. Springer-Verlag, 1975.
M. J. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.
D. Howe. The computational behaviour of Girard's paradox. Proc. of Second Symp. on Logic in Comp. Sci., IEEE, pages 205–214, June 1987.
D. J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.
D. J. Howe. Computational metatheory in Nuprl. Ninth Conference on Automated Deduction, pages 238–257, May 1988.
D. J. Howe. Equality in lazy computation systems. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 198–203. IEEE Computer Society, June 1989.
D. J. Howe. On computational open-endedness in Martin-Löf's type theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science. IEEE Computer Society, 1991.
P. B. Jackson. Developing a toolkit for floating-point hardware in the Nuprl proof development system. In Proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies. Elsevier, 1991.
P. B. Jackson. Nuprl and its use in circuit design. In V. Stavridou, T. Melham, and R. Boute, editors, Theorem Provers in Circuit Design, pages 311–336. North-Holland, 1992.
P. Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175, Amsterdam, 1982. North Holland.
P. Mendler. Inductive Definition on Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1988.
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.
C. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 96–107. IEEE Computer society, 1991.
B. Nördstrom, K. Petersson, and J. M. Smith. Programming in Martin-Löf's Type Theory, volume 7 of International Series of Monographs on Computer Science. Oxford Science Publications, 1990.
R. E. Shostak. On the SUP-INF method for proving Presburger formulas. J. ACM, 24(4):529–543, October 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Howe, D.J. (1993). Reasoning about functional programs in Nuprl. In: Lauer, P.E. (eds) Functional Programming, Concurrency, Simulation and Automated Reasoning. Lecture Notes in Computer Science, vol 693. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56883-2_9
Download citation
DOI: https://doi.org/10.1007/3-540-56883-2_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56883-4
Online ISBN: 978-3-540-47776-1
eBook Packages: Springer Book Archive