Paper: Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages (at LICS 1987)

Authors: Andreas Goerdt

Abstract

Denotational semantics allows us to translate many imperative languages into the language of finitely typed λ-terms. Applying our ^9,10 Hoare Calculus for typed λ-terms, we get Hoare Calculi for such languages in a uniform way. Completeness results for these calculi follow from the completeness result proved by the author^9,10.
We demonstrate our basic ideas for the language While, obtaining a calculus which is effectively equivalent to the classical Hoare Calculus for While. The same method as for While yields a Hoare Calculus for a language with higher type procedures and parameters standing for locations (reference parameters), the language L₄ from Clarke². This calculus is for Herbrand definable interpretations complete in the sense of Cook. This shows the power of our method, for, though Hoare Logic for higher type concepts in programming languages raised some interest in the literature^{4,5,6,7,8,12,13,14}, only the Hoare Calculus by German et al.^7,8 has similar (in fact slightly stronger) completeness properties as our calculus.

BibTeX

  @InProceedings{Goerdt-HoareLogicforLambda,
    author = 	 {Andreas Goerdt},
    title = 	 {Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {293--299 },
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }