Skip to main content
SpringerLink
Log in

Mathematics as programming

  • Conference paper
  • First Online:
Book cover Logics of Programs (Logic of Programs 1983)

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

Included in the following conference series:

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. Aczel, P., "The Type Theoretic Interpretation of Constructive Set Theory", Logic Colloquium '77, A. MacIntyre, L. Pacholaki and J. Paris (eds.), North-Holland, Amsterdam, 1978, 55–66.

    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.L. and R.L. Constable, "The Nearly Ultimate PRL", Department of Computer Science Technical Report TR 83-551, Cornell University, April 1983.

    Google Scholar 

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

    Google Scholar 

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

  6. Bourbaki, N., Elements of Mathematics, Vol I, Theory of Sets, Addison-Wesley, Reading, 1968.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

  10. Constable, Robert L., "Programs As Proofs", Department of Computer Science, Technical Report TR 82-532, Cornell University, 1982. (To appear in Information Processing Letters, 1983.)

    Google Scholar 

  11. Constable, Robert L. and D.R. Zaltin, "The Type Theory of PL/CV3", IBM Logic of Programs Conference, Lecture Notes in Computer Science, Vol. 131, Springer-Verlag, NY, 1982, 72–93.

    Google Scholar 

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

    Google Scholar 

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

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

    Google Scholar 

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

  16. Jensen, K. and N. Wirth. Pascal User Manual and Report. (2nd ed.), Springer-Verlag, New York, 1975.

    Google Scholar 

  17. Jutting, L.S., "Checking Landau's ‘Grundlagen’ in the AUTOMATH System" (Doctoral Thesis, Eindhoven University), Math. Centre Tracts No. 83, Math. Centre, Amsterdam, 1979.

    Google Scholar 

  18. Kleene, S.C., Introduction to Metamathematics, D. Van Nostrand, Princeton, 1952, 550 pp.

    Google Scholar 

  19. Machtey, Michael and P. Young, An Introduction to the General Theory of Algorithms, North-Holland, NY, 1978.

    Google Scholar 

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

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

  22. McGettrick, A.D., Algol 68, A First and Second Course, Cambridge University Press, Cambridge, 1978.

    Google Scholar 

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

  24. Reynolds, John C. "Towards a Theory of Type Structure", Proc. Colloque su, la Programmation, Lecture Notes in Computer Science, 19, Springer-Verlag, pp. 408–425, 1974.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  27. van Wijngaarden, A.B.J. et al, Revised Report on the Algorithmic Language ALGO 68, Supplement to ALGO BULLETIN, University of Alberta, 1974.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cornell University, USA

    R. L. Constable

Authors
  1. R. L. Constable
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Edmund Clarke Dexter Kozen

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Constable, R.L. (1984). Mathematics as programming. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_359

Download citation

  • DOI: https://doi.org/10.1007/3-540-12896-4_359

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-12896-0

  • Online ISBN: 978-3-540-38775-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation