Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Mathematical Foundations of Computer Science

MFCS 1979: Mathematical Foundations of Computer Science 1979 pp 146–159Cite as

Lcf: A way of doing proofs with a machine

  • Invited Lectures
  • Conference paper
  • First Online:

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Blikle, A., Specified Programming, ICS PAS Report 333, Inst. of Computer Science, Polish Academy of Sciences, Warsaw, 1978.

    Google Scholar 

  2. Burstall, R.M., and Goguen, J.A., Putting theories together to make specifications, Proc. 5th International Joint Conference on Artificial Intelligence, Cambridge Mass., published by Dept. Comp. Sci., Carnegie Mellon, 1045–1058, 1977.

    Google Scholar 

  3. Cohn, A., High level proof in LCF, Proc. 4th Workshop on Automated Deduction, Austin, Texas, 73–80, 1979.

    Google Scholar 

  4. Constable, R.L., and O'Donnell, M.J., A Programming Logic, Winthrop, 1978.

    Google Scholar 

  5. deBruijn, N.G., The mathematical language AUTOMATH, Symposium in Automatic Demonstration, Lecture Notes in Math, Vol. 125, Springer-Verlag, New York, 29–61, 1970.

    Google Scholar 

  6. Floyd, R.W., Assigning meanings to programs, Proc. Symposia in Applied Mathematics, Vol. XIX, Amer. Math. Soc., Providence, 19–32, 1967.

    Google Scholar 

  7. Giles, D.A., The theory of LISTS in LCF, Report CSR-31-78, Computer Science Dept., Edinburgh University, 1978.

    Google Scholar 

  8. Goodstein, R.L., Boolean Algebra, Pergamon Press, Macmillan Company, New York, 1963.

    Google Scholar 

  9. Gordon, M., Milner, R., Morris, L., Newey, M. and Wadsworth, C., A metalanguage for interactive proof in LCF, Proc. 5th ACM SIGACT-SIGPLAN Conference on Principles of Programming Languages, Tucson, Arizona, USA, 1978.

    Google Scholar 

  10. Gordon, M., Milner, R. and Wadsworth, C., Edinburgh LCF, Report CSR-11-77, Computer Science Dept., Edinburgh University, 1977.

    Google Scholar 

  11. Hewitt, C., PLANNER: a language for manipulating models and proving theorems in a robot, AI Memo 168, Project MAC, MIT, Cambridge, Mass., 1970.

    Google Scholar 

  12. Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, 12, 576–581, 1969.

    Article  Google Scholar 

  13. Milner, R. and Weyhrauch, R.W., Proving compiler correctness in a mechanized logic, Machine Intelligence 7, ed. B. Meltzer & D.Michie, Edinburgh University Press, 51–72, 1972.

    Google Scholar 

  14. Pratt, V.R., Semantical considerations on Floyd-Hoare logic, Proc. 17th Annual IEEE Symposium on Foundations of Computer Science, 109–121, 1976.

    Google Scholar 

  15. Rasiowa, H., Algorithmic Logic, Inst. of Computer Science, Polish Academy of Sciences, Warsaw, 1977.

    Google Scholar 

  16. Robinson, J.A., A machine-oriented logic based on the resolution principle, JACM, 12, 23–41, 1965.

    Article  Google Scholar 

  17. Scott, D., Data types as lattices, SIAM J. Computing, 5, 1976, 522–587.

    Article  Google Scholar 

  18. Scott, D. and Strachey, C., Towards a mathematical semantics for computer languages, Proc. Symposium on Computers and Automata, Vol.21, Microwave Research Inst. Symposia Series, Polytech. Inst. of Brooklyn, New York, 19–46, 1971.

    Google Scholar 

  19. Van Emden, M.H. and Kowalski, R.A., The semantics of predicate logic as a programming language, J.ACM, 23, 733–742, 1976.

    Article  Google Scholar 

  20. Weyhrauch, R.W., Prolegomena to a theory of formal reasoning, Memo AIM-315, Computer Science Dept., Stanford University, 1978.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Edinburgh, King's Buildings, Mayfield Road, EH9 3JZ, Edinburgh, Scotland

    Robin Milner

Authors
  1. Robin Milner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jiří Bečvář

Rights and permissions

Reprints and permissions

Copyright information

© 1979 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Milner, R. (1979). Lcf: A way of doing proofs with a machine. In: Bečvář, J. (eds) Mathematical Foundations of Computer Science 1979. MFCS 1979. Lecture Notes in Computer Science, vol 74. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-09526-8_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-09526-8_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-09526-2

  • Online ISBN: 978-3-540-35088-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation