Hoare logic and lambda calculus

• To: types@theory.LCS.MIT.EDU
• Subject: Hoare logic and lambda calculus
• From: rdt%QUCIS.BITNET@mitvma.mit.edu
• Date: Tue, 11 Oct 88 10:29:10 EDT
• Sender: meyer@theory.LCS.MIT.EDU

Date: Tue, 11 Oct 88 09:39:52 EDT

To: types@theory.LCS.MIT.EDU

Dennis Kfoury complains that there is "an unavoidable break" between
these two subjects.  Not so.  Hoare logic can be presented as
a quantifier-free fragment of multi-sorted predicate logic
(with Hoare triples as atomic formulas).  Then add procedures and
generalize to Reynolds's specification logic.  The axioms for the
lambda calculus can then be treated.  I am using this approach
in my chapter on Denotational Semantics of Algol-like Languages in
the Handbook of Logic in Computer Science.  A preliminary draft of
this is available from me in return for comments, corrections and
suggestions for improvement.

• Prev: Re: teach untyped lambda calculus?
• Next: Un/typed lambda calculus
• Index(es):
  • Main
  • Thread