Imperative Program Semantics

by Stuart F. Allen
1994-1995

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.

Imperative Program Semantics

by Stuart F. Allen 1994-1995

by Stuart F. Allen
1994-1995