Deep semantic embedding of PSL (Sugar 2.0) in HOL
The main properties proved so far are here.
The full details are in the HOL script files below. These are the current working version
at Cambridge. Every so often I check consistent versions into the
SourceForge repository.
- Definition of Kripke structures
- Definition of finite paths (lists)
- Definition of infinite paths
- Definition of abstract syntax
- Definition of unclocked semantics
- Definition of clocked semantics
- Definition of rewrites
- Theorems proved about PSL semantics
MICHAEL J. C. GORDON
University of Cambridge
Computer Laboratory
Room FE19
William Gates Building
JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
work phone: +44 1223 334627
work fax: +44 1223 334678
email: mjcg@cl.cam.ac.uk