Presenting Formal Semantics for a
Presenting Java in Nuprl
Presenting Java in Nuprl
J Fragment of Java
J Fragment of Java
Presenting Java in Nuprl
J Semantics
State of a J Virtual Machine
class RecPair {int z; RecPair r}
Presenting Java in Nuprl
Reference Object Theory
Reference Object Theory
Reference Object Theory
Reference Object Theory
Reference Object Theory
Type Theory + Object Theory = ?
Presenting Java in Nuprl
Verification Results
Formal Verification
Presenting Java in Nuprl
De-formalization
Formal Proof Structure
Results
Download
slide show file