# Reasoning about functional programs in Nuprl

Chapter

First Online:

## 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.

## Keywords

IEEE Computer Society Type Theory Induction Rule Proof Tree Majority Candidate
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- 1.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.Google Scholar - 2.S. F. Allen.
*A Non-Type-Theoretic Semantics for Type-Theoretic Language*. PhD thesis, Cornell University, 1987.Google Scholar - 3.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.Google Scholar - 4.R. Backhouse. Algorithm development in Martin-Löf's type theory. Technical report, University of Essex, 1984.Google Scholar
- 5.D. A. Basin and P. Delvecchio. Verification of combinational logic in Nuprl. In
*Hardware Specification, Verification and Synthesis: Mathematical Aspects*, Ithaca, New York, 1989.Google Scholar - 6.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.Google Scholar - 7.R. Boyer and J. Moore. MJRTY, a fast majority vote algorithm. Technical report, University of Texas at Austin, 1981.Google Scholar
- 8.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.Google Scholar - 9.R. Constable and D. Howe. Nuprl as a general logic. In P. Odifreddi, editor,
*Logic in Computer Science*, pages 77–90. Academic Press, 1990.Google Scholar - 10.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).Google Scholar - 11.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.Google Scholar - 12.R. L. Constable, et al.
*Implementing Mathematics with the Nuprl Proof Development System*. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.Google Scholar - 13.T. Coquand and G. Huet. The Calculus of Constructions.
*Information and Computation*, 76:95–120, 1988.Google Scholar - 14.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.Google Scholar - 15.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.Google Scholar - 16.D. Howe. The computational behaviour of Girard's paradox.
*Proc. of Second Symp. on Logic in Comp. Sci., IEEE*, pages 205–214, June 1987.Google Scholar - 17.D. J. Howe.
*Automating Reasoning in an Implementation of Constructive Type Theory*. PhD thesis, Cornell University, 1988.Google Scholar - 18.D. J. Howe. Computational metatheory in Nuprl.
*Ninth Conference on Automated Deduction*, pages 238–257, May 1988.Google Scholar - 19.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.Google Scholar - 20.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.Google Scholar - 21.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.Google Scholar - 22.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.Google Scholar - 23.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.Google Scholar - 24.P. Mendler.
*Inductive Definition on Type Theory*. PhD thesis, Cornell University, Ithaca, NY, 1988.Google Scholar - 25.R. Milner, M. Tofte, and R. Harper.
*The Definition of Standard ML*. MIT Press, 1990.Google Scholar - 26.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.Google Scholar - 27.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.Google Scholar - 28.R. E. Shostak. On the SUP-INF method for proving Presburger formulas.
*J. ACM*, 24(4):529–543, October 1977.Google Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1993