Skip to main content
SpringerLink
Log in

A Hoare Calculus for functions defined by recursion on higher types

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

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

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. E.M. Clarke, Programming language constructs for which it is impossible to obtain good Hoare — like axioms, JACM 26, 129–147, (1979)

    Google Scholar 

  2. E.M. Clarke, S.M. German, J.Y. Halpern, On effective axiomatizations of Hoare logics, Proceedings 9th POPL, 309–321, (1982)

    Google Scholar 

  3. W. Damm, B. Josko, A sound and relatively* complete Hoare-Logic for a language with higher type procedures, Acta Informatica 20, 59–101, (1983)

    Google Scholar 

  4. J.W. deBakker, J.-J.Ch. Meyer, J.W. Klop, Correctness of programs with function procedures, Proceedings Logics of programs, LNCS 134, 94–112, (1982)

    Google Scholar 

  5. G.W. Ernst, J.K. Navlakha, W.F. Ogden, Verification of programs with procedure type parameters, Acta Informatica 18, 149–169, (1982)

    Google Scholar 

  6. S.M. German, E.M. Clarke, J.Y. Halpern, Reasoning about procedures as parameters, Proceedings Logics of programs, LNCS 164, 206–220, (1983)

    Google Scholar 

  7. A. Goerdt, Ein Hoare Kalkül für getypte λ-Terme — Korrektheit, Vollständigkeit, Anwendungen, RWTH Aachen

    Google Scholar 

  8. B. Josko, On expressive interpretations of a Hoare-logic for Clarke's language L 4, STACS 1984, LNCS 166, 73–84, (1984)

    Google Scholar 

  9. A. Kanda, Effektive solutions of recursive domain equations, Thesis Warwick, (1979)

    Google Scholar 

  10. H. Langmaack, Aspects of programs with finite modes, FCT 83, LNCS 158, 241–254, (1983)

    Google Scholar 

  11. E.-R. Olderog, Correctness of programs with PASCAL — like procedures without global variables, TCS 30, 49–90, (1984)

    Google Scholar 

  12. M. Sintzoff, Proof — oriented and applicative valuations in definitions of algorithms, Proceedings of the 1981 Conference on Functional Programming Languages and Computer Architecture, 155–162, (1981)

    Google Scholar 

  13. P. Urzyczyn, A necessary and sufficient condition in order that a Herbrand interpretation is expressive relative to recursive programs, Information and Control 56, 212–219, (1983)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lehrstuhl für Informatik II RWTH Aachen, Büchel 29 — 31, D-5100, Aachen, West-Germany

    Andreas Goerdt

Authors
  1. Andreas Goerdt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rohit Parikh

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Goerdt, A. (1985). A Hoare Calculus for functions defined by recursion on higher types. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-15648-8_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation