Imperative Program Semantics
by Stuart F. Allen
Stuart Allen will discuss the imperative program semantics he has been working on in Nuprl. Some CS611 concepts are relevant, and it is intended as a target language for Polya programs.
After an introduction to the material, a short demo will be given using the Nuprl edit environment to examine a (partial) proof pertaining to interpreting such programs, with emphasis on features of the environment and methods using it.