-
Notifications
You must be signed in to change notification settings - Fork 8
Logics
Attila Sukosd edited this page Mar 15, 2013
·
1 revision
One of our end-user panel described MOBIUS as having a menagerie of logics.
WikiInclude(LogicsExplanation)
MOBIUS base logic is the core program logic for bytecode and it relies on Bicolano JVM semantics. It is formalised with the Coq proof assistant. Its bundle with Coq files can be downloaded here and checked with Coq 8.0pl3.
http://mobius.inria.fr/twiki/bin/view/Mobius/MobiusTutorial
Version: 1 Time: Wed Jun 25 13:51:58 2008 Author: dcochran (dcochran) IP: 193.1.132.32