Skip to main content
SpringerLink
Log in

Metalevel Programming in Constructive Type Theory

  • Conference paper
Programming and Mathematical Method

Part of the book series: NATO ASI Series ((NATO ASI F,volume 88))

Abstract

This paper describes a particular version of constructive type theory, a subset of the one underlying the Nuprl proof development system, and it examines its role as a programming environment. Special attention is given to the property of the theory to talk about itself. This reflective capability is the basis for automating proof development and for metalevel programming.

(This research supported by NSF grant CCR86-16552 and ONR grant N00014-88K-0490.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Allen, R. Constable, and D. Howe. Reflecting the open-ended computation system of constructive type theory. In Algebra, Logic and Computation. NATO ASI Series, 1990.

    Google Scholar 

  2. S. Allen, R. Constable, D. Howe, and W. Aitken. The semantics of reflected proof. Proc. of Fifth Symp. on Logic in Comp. Sci., IEEE, June 1990.

    Google Scholar 

  3. S. F. Allen. A non-type-theoretic semantics for type-theoretic language. PhD thesis, Cornell University, 1987.

    Google Scholar 

  4. P. Audebaud. Partial objects in the calculus of constructions. In Sixth Symp. on Logic in Computer Science, IEEE, Vrije University, Amsterdam, The Netherlands, 1991.

    Google Scholar 

  5. D. Basin and R. Constable. Meta-logical frameworks. In Proc. of the Second Workshop on Logical Frameworks, Edinburgh, UK, June 1991.

    Google Scholar 

  6. J. L. Bates. A logic for correct program development PhD thesis, Cornell University, 1979.

    Google Scholar 

  7. E. Bishop and D. Bridges. Constructive Analysis. NY:Springer-Verlag, 1985.

    Book  MATH  Google Scholar 

  8. W. Bledsoe and D. Loveland. Automated Theorem Proving: After 25 Years. American Math Soc, 1984.

    Google Scholar 

  9. R. Boyer and J. Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. In The Correctness Problem in Computer Science, pages 103–84. NY:Academic Press, 1981.

    Google Scholar 

  10. W. Buchholtz et al. Iterated inductive definitions and subsystems of analysis. Recent Proof-Theoretical Studies, Lecture Notes in Mathematics, 897, 1981.

    Google Scholar 

  11. A. Bundy. The Computer Modelling of Mathematical Reasoning. NY:Academic Press, 1983.

    MATH  Google Scholar 

  12. A. Bundy. A broader interpretation of logic in logic programming. In Proc. 5th Sympo. on Logic Programming, 1988.

    Google Scholar 

  13. R. Constable and N. Mendler. Recursive Definitions in Type Theory. In Proc. of Logics of Prog. Conf, pages 61–78, January 1985. Cornell TR 85-2013;659.

    Google Scholar 

  14. R. Constable and S. F. Smith. Computational foundations of basic function theory. In Third Symp. on Logic in Somp. Sci. IEEE, 1988. (Cornell TR 88-904).

    Google Scholar 

  15. R. L. Constable et al. Implementing Mathematics with the Nuprl Development System. NJ:Prentice-Hail, 1986.

    Google Scholar 

  16. R. L. Constable and D. J. Howe. Implementing metamathematics as an approach to automatic theore m proving. In R. Banerji, editor, Formal Techniques in Artificial Intelligence: A Source Boo k, pages 45–76. Elsevier Science Publishers (North-Holland), 1990.

    Google Scholar 

  17. T. Coquand and G. Huet. The calculus of construction. Information and Computation, 76:95–120 , 1988.

    Article  MATH  MathSciNet  Google Scholar 

  18. T. Coquand and C. Paulin-Mohring. Inductively defined types, preprint.

    Google Scholar 

  19. M. Davis and J. T. Schwartz. Metamathematical extensibility for theorem verifiers and proof checkers. Comp. Math, with Applications, 5:217–230, 1979.

    Article  MATH  MathSciNet  Google Scholar 

  20. P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics. In Proceedings of the B.R.A. Workshop on Logical Frameworks, Sophia-Antipolis, France, June 1990. (To appear.).

    Google Scholar 

  21. S. Feferman. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In Proc. Conf. Intuitionism and Proof Theory, pages 303–326, Buffalo, NY, 1970. North-Holland.

    Google Scholar 

  22. J. Gallier. Logic for computer science. In Foundations of Automatic Theorem Proving. Harper and Row, 1986.

    Google Scholar 

  23. J.-Y. Girard. Une extension de l’interprétation de godel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la théorie des types. In 2nd Scandinavian Logic Symp., pages 63–69. NY:Springer-Verlag, 1971.

    Chapter  Google Scholar 

  24. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1988.

    Google Scholar 

  25. M. Gordon. Hol: A machine oriented formalization of higher order logic. Technical report, Cambridge University, 1985. TR 68.

    Google Scholar 

  26. M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: a mechanized logic of computation. Lecture Notes in Computer Science, 78, 1979.

    Google Scholar 

  27. T. Griffin. A formulas-as-types notion of control. In POPL, 1990.

    Google Scholar 

  28. S. Hayashi and H. Nakano. PX: A Computational Logic. Foundations of Computing. MIT Press, Cambridge, MA, 1988.

    Google Scholar 

  29. D. Howe and J. Chirimar. Nuprl mathematics library, unpublished, 1989.

    Google Scholar 

  30. D. J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.

    Google Scholar 

  31. D. J. Howe. Equality in lazy computation systems. Proc. Fourth Symp. Logic in Computer Science, IEEE, 1989.

    Google Scholar 

  32. T. B. Knoblock and R. L. Constable. Formalized metareasoning in type theory. In Proc. of the First Annual Symp. on Logic in Computer Science. IEEE , 1986.

    Google Scholar 

  33. J. Lipton. Logic programming in the nuprl type theory environment. Technical report, Cornell University, Ithaca, NY, 1991. To appear as a technical report, summer 1991.

    Google Scholar 

  34. Z. Luo. Ecc, an extended calculus of construction. In Proc. Fourth Symp. on Logics in Computer Science, IEEE, Washington, DC, June 1989.

    Google Scholar 

  35. P. Martin-Lof. An intuitionistic theory of types: predicative part. In Logic Colloquium ’73., pages 73–118. Amsterdam:North-Holland, 1973.

    Google Scholar 

  36. P. Martin-Lof. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–75. Amsterdam:North Holland, 1982.

    Chapter  Google Scholar 

  37. P. Mendier. Recursive Types and Type Constraints in Second-Order Lambda Calculus. Proc. in Second Symp. on Logic in Comp. Sci., IEEE, pages 30–36, June 1987.

    Google Scholar 

  38. P. Mendier. Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1988.

    Google Scholar 

  39. D. Miller and G. Nadathur. A logic programming approach to manipulating formulas and programs. In IEEE Symp. on Logic Programming. ACM, 1987.

    Google Scholar 

  40. C. Murthy. Extracting Constructive Content for Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. TR 89-1151.

    Google Scholar 

  41. C. Murthy. An evaluation semantics for classical proofs. In LICS, ’91, Amsterdam, The Netherlands, July 1991.

    Google Scholar 

  42. C. Murthy and J. Russell. A constructive proof of higman’s lemma. Technical Report TR 89-1049, Cornell University, Ithaca, NY 14853, January 1989.

    Google Scholar 

  43. B. Nordstrom, K. Peterson, and J. Smith. Programming in Martin-Lof’s Type Theory. Oxford Sciences Publication, Oxford, 1990.

    Google Scholar 

  44. C. Paulin-Mohring. Extraction in the calculus of constructions. PhD thesis, University of Paris VII, 1989.

    Google Scholar 

  45. F. Pfenning. Elf: a language for logic definition and verfied metaprogramming. LICS, pages 313–321, 1989.

    Google Scholar 

  46. N. Shanker. Towards mechanical metamathematics. J. Automated Reasoning, l(4):407–434, 1985.

    Google Scholar 

  47. S. Smith. Partial Objects in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1989.

    Google Scholar 

  48. S. Smith and R. L. Constable. Partial objects in constructive type theory. In Symposium on Logic in Computer Science., pages 183–93. Washington, D.C.:IEEE., 1987.

    Google Scholar 

  49. R. M. Smullyan. First-Order Logic. Springer-Verlag, New York, 1968.

    MATH  Google Scholar 

  50. A. Troelstra. Metamathematical investigation of intuitionistic mathematics. Lecture Notes in Mathematics, 344, 1973.

    Google Scholar 

  51. R. Weyrauch. Prolegomena to a theory of formal reasoning. Artificial Intelligence, 13:133–170., 1980.

    Article  MathSciNet  Google Scholar 

  52. L. Wos, R. Overbeek, L. Ewing, and J. Boyle. Automated Reasoning. Prentice-Hall, Englewood Cliffs, NJ, 1984.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, Ithaca, NY, 14853, USA

    Robert L. Constable

Authors
  1. Robert L. Constable
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Technische Universität München, Postfach 202420, München 2, W-8000, Germany

    Manfred Broy

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Constable, R.L. (1992). Metalevel Programming in Constructive Type Theory. In: Broy, M. (eds) Programming and Mathematical Method. NATO ASI Series, vol 88. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-77572-7_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-77572-7_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-77574-1

  • Online ISBN: 978-3-642-77572-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation