Advertisement

Reasoning about functional programs in Nuprl

  • Douglas J. Howe
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 693)

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.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    S. F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987.Google Scholar
  3. 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. 4.
    R. Backhouse. Algorithm development in Martin-Löf's type theory. Technical report, University of Essex, 1984.Google Scholar
  5. 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. 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. 7.
    R. Boyer and J. Moore. MJRTY, a fast majority vote algorithm. Technical report, University of Texas at Austin, 1981.Google Scholar
  8. 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. 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. 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. 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. 12.
    R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.Google Scholar
  13. 13.
    T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76:95–120, 1988.Google Scholar
  14. 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. 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. 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. 17.
    D. J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.Google Scholar
  18. 18.
    D. J. Howe. Computational metatheory in Nuprl. Ninth Conference on Automated Deduction, pages 238–257, May 1988.Google Scholar
  19. 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. 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. 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. 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. 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. 24.
    P. Mendler. Inductive Definition on Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1988.Google Scholar
  25. 25.
    R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.Google Scholar
  26. 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. 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. 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

Authors and Affiliations

  • Douglas J. Howe
    • 1
  1. 1.Department of Computer ScienceCornell UniversityIthacaUSA

Personalised recommendations