Skip to main content
SpringerLink
Log in

Comstructive matnkmatics as a programming logic I: Some principles of theory

  • Conference paper
  • First Online:
Foundations of Computation Theory (FCT 1983)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 158))

Included in the following conference series:

Abstract

The design of a programming system is guided by certain beliefs, principles and practical constraints. These considerations are not always manifest from the rules defining the system. In this paper the author discusses some of the principles which have guided the design of the programming logics built at Cornell in the last decade. Most of the necessarily brief discussion concerns type theory with stress on the concepts of function space and quotient types.

This work was supported in part by NSF grants MCS-80-03349 and MCS-81-04018.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bates, J.L., A Logic for Correct Program Development, Ph.D. Thesis, Department of Computer Science, Cornell University, 1979.

    Google Scholar 

  2. Bates, J.L. and R.L. Constable, "Proofs as Programs", Dept. of Computer Science Technical Report, TR 82-530, Cornell University, Ithaca, NY, 1982.

    Google Scholar 

  3. Bates J. and R.L. Constable, "Definition of Micro-PRL", Technical Report TR 82-492, Computer Science Department, Cornell University, October 1981.

    Google Scholar 

  4. Beeson, M., "Formalizing Constructive Mathematics: Why and How?", Constructive Mathematics (ed., F. Richman), Lecture Notes in Computer Science, Springer-Verlag, NY, 1981, 146–190.

    Google Scholar 

  5. Bishop, E., Foundations of Constructive Analysis, McGraw Hill, NY, 1967, 370 pp.

    Google Scholar 

  6. Bishop, Errett, "Mathematics as a Numerical Language", Intuitionism and Proof Theory, ed. by Myhill, J. et al., North-Holland, Amsterdam, 1970, 53–71.

    Google Scholar 

  7. Boyer, R.S. and J.S. Moore, A Computational Logic, Academic Press, NY, 1979, 397 pp.

    Google Scholar 

  8. Constable, Robert L., "Constructive Mathematics and Automatic Program Writers", Proc. of IFIP Congress, Ljubljana, 1971, pp 229–233.

    Google Scholar 

  9. Constable, Robert L. and David Gries, "On Classes of Program Schemata", SIAM J. Comput., 1:1, March 1972, pp. 66–118.

    Article  Google Scholar 

  10. Constable, Robert L., "Mathematics As Programming", Proc. of Workshop on Logics of Programs, Lecture Notes in Computer Science, 1983.

    Google Scholar 

  11. Constable, Robert L., "Partial Functions in Constructive Formal Theories", Proc. of 6th G.I. Conference, Lecture Notes in Computer Science, Vol. 135. Springer-Verlag, 1983.

    Google Scholar 

  12. Constable, Robert L., "Intensional Analysis of Functions and Types", University of Edinburgh, Dept. of Computer Science Internal Report, CSR-118-82, June, 1982, pp. 74.

    Google Scholar 

  13. Constable, Robert L. and D. Zlatin, "Report on the Type Theory (V3) of the Programming Logic PL/CV3", Logics of Programs, Lecture Notes in Computer Science, Vol. 131, Springer-Verlag, NY, 1982, pp. 72–93.

    Google Scholar 

  14. Constable, R.L., "Programs and Types", Proc. of 21st Ann. Symp. on Found. of Comp. Science, IEEE, NY, 1980, pp 118–128.

    Google Scholar 

  15. Constable, Robert L. and M.J. O'Donnell, A Programming Logic, Winthrop, Cambridge, 1978.

    Google Scholar 

  16. Constable, Robert L., S.D. Johnson and C.D. Eichenlaub, Introduction to the PL/CV2 Programming Logic, Lecture Notes in Computer Science, Vol. 135, Springer-Verlag, NY, 1982.

    Google Scholar 

  17. Curry, H.B. and R. Feys, Combinatory Logic, North-Holland, Amsterdam, 1968.

    Google Scholar 

  18. Curry, H.B., J.R. Hindley, and J.P. Seldin, Combinatory Logic, Volume II, North-Holland Publ. Co., Amsterdam, 1972.

    Google Scholar 

  19. deBruijn, N.G., "A Survey of the Project AUTOMATH", Essays on Combinatory Logic, Lambda Calculus and Formalism, (eds. J.P. Seldin and J.R. Hindley), Academic Press, NY, 1980, 589–606.

    Google Scholar 

  20. Donahue, J., and A.J. Demers, "Revised Report on Russell". Department of Computer Science Technical Report, TR 79-389, Cornell University, September 1979.

    Google Scholar 

  21. Dummett, Michael, Frege Philosophy of Language, Duckworth, Oxford, 1973.

    Google Scholar 

  22. Feferman, S., "Constructive Theories of Functions and Classes", Logic Colloquium '78, North-Holland, Amsterdam, 1979, pp. 159–224.

    Google Scholar 

  23. Fraenkel, A.A., and Y. Bar-Hillel, Foundations of Set Theory, North-Holland Publ. Co., Amsterdam, 1958.

    Google Scholar 

  24. Gordon, M., R. Milner and C. Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, Vol. 78, Springer-Verlag, 1979.

    Google Scholar 

  25. Gries, David, The Science of Programming, Springer-Verlag, 1982.

    Google Scholar 

  26. Howard, W.A., "The Formulas-As-Types Notion of Construction" in Essays on Combinatory Logic, Lambda Calculus and Formalism, (eds., J.P. Seldin and J.R. Hindley), Academic Press, NY, 1980.

    Google Scholar 

  27. Krafft, Dean B., "AVID: A System for the Interactive Development of Verifiable Correct Programs", Ph.D. Thesis, Cornell University, Ithaca, NY, August 1981.

    Google Scholar 

  28. Luckham, D.C., M.R. Park, and M.S. Paterson, "On Formalized Computer Programs", JCSS, 4, 1970, pp. 220–249.

    Google Scholar 

  29. Martin-Löf, Per, "An Intuitionistic Theory of Types: Predicative Part", Logic Colloquium, 1973, (eds. H.E. Rose and J.c. Shepherdson), North-Holland, Amsterdam, 1975, 73–118.

    Google Scholar 

  30. Martin-Löf, Per, "Constructive Mathematics and Computer Programming", 6th International Congress for Logic, Method and Phil. of Science, North-Holland, Amsterdam, 1982.

    Google Scholar 

  31. Nordstrom, B., "Programming in Constructive Set Theory: Some Examples", Proc. 1981 Conf. on Functional Prog. Lang. and Computer Archi, Portsmouth, 1981, 141–153.

    Google Scholar 

  32. Pratt, Terrence W., Programming Languages: Design and Implementation, Prentice-Hall, Englewood Cliffs, 1975, 530p.

    Google Scholar 

  33. Russell, B., "Mathematical Logic as Based on a Theory of Types", Am. J. of Math., 30, 1908, pp. 222–262.

    Google Scholar 

  34. Scott, Dana, "Data Types as Lattices". SIAM Journal on Computing, Vol. 5, No. 3, September, 1976.

    Google Scholar 

  35. Scott, Dana, "Constructive Validity", Symposium on Automatic Demonstration, Lecture Notes in Mathematics, 125, Springer-Verlag, 1970, 237–275.

    Google Scholar 

  36. Stenlund, S., Combinators, Lambda-terms, and Proof-Theory, D. Reidel, Dordrecht, 1972, 183 pp.

    Google Scholar 

  37. Skolem, T., "Begründung der elementären Arithmetik durch die Rekurrierende Denkweise ohne Anwendung scheinbarer Varanderlichen mit unendlichen Ausdehnunggsbereich, Videnskapsselskapets Skrifter 1, Math-Naturv K16, 1924, 3–38, (also in From Frege to Gödel, p. 302–333 and in Skolem's Selected Works in Logic ed., J.E. Fenstad, Oslo, 1970).

    Google Scholar 

  38. Teitelbaum, R. and T. Reps, "The Cornell Program Synthesizer: A Syntax-Directed Programming Environment", CACM, 24:9, September 1981, 563–573.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Cornell University, 14853, Ithaca, N.Y.

    Robert L. Constable

Authors
  1. Robert L. Constable
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marek Karpinski

Rights and permissions

Reprints and permissions

Copyright information

© 1983 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Constable, R.L. (1983). Comstructive matnkmatics as a programming logic I: Some principles of theory. In: Karpinski, M. (eds) Foundations of Computation Theory. FCT 1983. Lecture Notes in Computer Science, vol 158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12689-9_94

Download citation

  • DOI: https://doi.org/10.1007/3-540-12689-9_94

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-12689-8

  • Online ISBN: 978-3-540-38682-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation