References:
Higher order logic (HOL)
Isar - Intelligible semi-automated reasoning.
Structured Proof Language.
Arithmetic Expressions:
| Concrete | Abstract |
|---|---|
| 5 | N 5 (constants) |
| x | V “x” (variables) |
| x + y | Plus (V “x”) (V “y”) |
| 2 + (z + 3) | Plus (N 2) (Plus (V “z”) (N 3)) |
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?