Simple Imperative Programming Language 
Abstract:
Author:
Theory Dependencies:
 Nuprl 4.2 with sexp_1 theory
|
expression
|
boolean expression
|
command
|
transition
|
hoare
|
hoare_examples
|
rules_3
|
natural
|
shadow
Theory Descriptions:

References:

  1. Semantics of Programming Languages: Structures and Techniques, Carl A. Gunter, MIT Press, 1992
  2. Mathematical Theory of Program Correctness, Jaco de Bakker, Prentice Hall, 1980
  3. Procedures and Parameters: An Axiomatic Approach, C.A.R. Hoare, in Lecture Notes in Mathematics 188, Springer, 1971