A Hoare Calculus for functions defined by recursion on higher types

This publication has 10 references indexed in Scilit:

• Correctness of programs with Pascal-like procedures without global variables
  Theoretical Computer Science, 1984
• Reasoning about procedures as parameters
  Lecture Notes in Computer Science, 1984
• A sound and relatively complete Hoare-logic for a language with higher type procedures
  Acta Informatica, 1983
• A necessary and sufficient condition in order that a Herbrand interpretation be expressive relative to recursive programs
  Information and Control, 1983
• On effective axiomatizations of Hoare logics
  Published by Association for Computing Machinery (ACM) ,1982
• Verification of programs with procedure-type parameters
  Acta Informatica, 1982
• Correctness of programs with function procedures
  Published by Springer Nature ,1982
• Proof-oriented and applicative valuations in definitions of algorithms
  Published by Association for Computing Machinery (ACM) ,1981
• Fully effective solutions of recursive domain equations
  Published by Springer Nature ,1979
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
  Journal of the ACM, 1979