Atc-theorem-generation
Facilities for generating theorems in ATC.
These are for the new approach to proof generation
in which we generate modular, compositional theorems.
Subtopics
- Atc-gen-new-inscope
- Generate an updated symbol table according to given criteria.
- Atc-gen-expr-bool-correct-thm
- Generate a correctness theorem for a boolean expression execution.
- Atc-gen-if/ifelse-inscope
- Generate an updated symbol table according to
executing a conditional statement.
- Atc-gen-expr-pure-correct-thm
- Generate a correctness theorem for a pure expression execution.
- Atc-gen-vardecl-inscope
- Generate an updated symbol table according to
declaring a new local variable.
- Atc-gen-enter-inscope
- Generate an updated symbol table according to entering a new scope.
