Skip to main content
SpringerLink
Log in

Proving program correctness in LCF

  • Justification Des Programmes Program Correctness
  • Conference paper
  • First Online:
Programming Symposium

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

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

  • Aiello, L., Aiello, M. and Weyhrauch, R.W., "The Semantics of PASCAL in LCF", Artificial Intelligence Memo No. 221 Stanford University (1973).

    Google Scholar 

  • Dijkstra, E.W., "Notes on Structured Programming", Structured Programming, by Dahl, O.J., Dijkstra, E.W. and Hoare, C.A.R., Academic Press, 1–82 (1972).

    Google Scholar 

  • Hoare, C.A.R. and Wirth, N. "An Axiomatic Definition of the Programming Language PASCAL", Eidg. Technische Hochschule, Zurich, Berichte der Fachgr, Computer-Wissenschaften, Nr. 6 (1972) also in Acta Informatica 2, 335–355 (1973).

    Google Scholar 

  • Igarashi, S., London, R.L. and Luckham D.C., "Automatic Program Verification I: A Logical Basis and its Implementation", Artificial Intelligence Memo No. 200, Stanford University (1973).

    Google Scholar 

  • Knuth, D., "The Art of Computer Programming", Addison Wesley Pub. Comp. (1968).

    Google Scholar 

  • Milner, R., "Logic for Computable Functions: Description of a Machine Implementation", Artificial Intelligence Memo No. 169, Stanford University (1972a).

    Google Scholar 

  • Milner, R., "Implementation and Applications of Scott's Logic for Computable Functions", Proc. ACM Conf. on Proving Assertions about Programs. New Mexico State University, Las Cruces, New Mexico, 1–5 (1972b).

    Google Scholar 

  • Milner, R. and Weyhrauch, R.W., "Proving Compiler Correctness in a Mechanized Logic", Machine Intelligence 7 (Meltzer, B. and Michie, D. Eds.), Edinbourgh University Press, 51–70 (1972).

    Google Scholar 

  • Newey, M., "Axioms and Theorems for Integers, Lists and Finite Sets in LCF", Artificial Intelligence Memo No. 184, Stanford University (1973).

    Google Scholar 

  • Newey, M., "Formal Semantics of LISP with Application to Program Correctness" Ph. D. Thesis, Stanford University (1974).

    Google Scholar 

  • Scott, D.S. and Strachey, C., "Towards a Mathematical Semantics for Computer Languages", Proc. of the Symposium on Computers and Automata, Microwave Research Institute Symposia Series, Vol.21, Polytechnic Institute of Brooklyn (1971).

    Google Scholar 

  • Wirth, N., "The Programming Language PASCAL", Acta Informatica 1, 35–63 (1971).

    Google Scholar 

  • Weyhrauch, R.W. and Milner, R., "Program Semantics and Correctness in a Mechanized Logic", Proc. 1st USA-Japan Computer Conf., Tokyo (1972).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Artificial Intelligence Laboratory, Stanford University, California

    Luigia Aiello & Mario Aiello

  2. Istituto di Elaborazione dell'Informazione, CNR, Pisa, Italy

    Luigia Aiello

  3. Instituto di Scienze dell'Informazione, Universita di Pisa, Italy

    Mario Aiello

Authors
  1. Luigia Aiello
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mario Aiello
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

B. Robinet

Rights and permissions

Reprints and permissions

Copyright information

© 1974 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aiello, L., Aiello, M. (1974). Proving program correctness in LCF. In: Robinet, B. (eds) Programming Symposium. Lecture Notes in Computer Science, vol 19. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-06859-7_124

Download citation

  • DOI: https://doi.org/10.1007/3-540-06859-7_124

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-06859-4

  • Online ISBN: 978-3-540-37819-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation