[Prev][Next][Index][Thread]
comments on my course outline
Date: Wed, 5 Oct 88 17:07:45 PDT
To: kfoury%bu-cs.BU.EDU@bu-it.bu.edu
Cc: jcm@ra.stanford.edu, types@theory.LCS.MIT.EDU
Thanks for your comments about the course. Since we
are on the quarter system, I am really pressed for
time, and cannot even be sure of covering everything
I have listed here.
If I were writing a text book, I suppose I might
include some Hoare logic. However, I am a bit
out of the subject now (maybe most other
people are too), so I am not sure what would be considered
essential. Do you think soundness and relative completeness
for WHILE programs, plus a discussion of Clarke's thesis
and decidability over finite interpretations covers it?
My first impression is that Hoare logic is almost completely
orthogonal to most of what I cover. Type theory becomes
interesting with higher-order functions, which is where
Hoare logic starts to fall apart. Howewver, there may be
some connection using Church's type theory (an old idea
of Albert's) which could be used to pull things together.
Another point is that the Scott-Strachey approach
translates programs with side-effects into functional
programs, allowing side-effects to be studied within the
framework of typed lambda calculus. (Of course, there are
known shortcomings of this approach.)
John