PRL Seminars

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.