Correctness of programs with function procedures

This publication has 16 references indexed in Scilit:

• A mathematical semantics for a nondeterministic typed λ-calculus
  Theoretical Computer Science, 1980
• The Semantics of Call-By-Value and Call-By-Name in a Nondeterministic Environment
  SIAM Journal on Computing, 1980
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
  Journal of the ACM, 1979
• Soundness and Completeness of an Axiom System for Program Verification
  SIAM Journal on Computing, 1978
• LCF considered as a programming language
  Theoretical Computer Science, 1977
• Even Simple Programs Are Hard To Analyze
  Journal of the ACM, 1977
• Least fixed points revisited
  Theoretical Computer Science, 1976
• Remarks on ?program proving: Jumps and functions by M. Clint and C. A. R. Hoare?
  Acta Informatica, 1976
• An axiomatic basis for computer programming
  Communications of the ACM, 1969
• Intensional interpretations of functionals of finite type I
  The Journal of Symbolic Logic, 1967