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

**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 _{4}* from
Clarke

^{2}. 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} }