Skip to topic
|
Skip to bottom
IST-15905
Mobius
Home
Objectives
Partners
Workpackages
End User Panel
Scientific Advisory Board
Publications
Deliverables
Links to Related projects
Intranet
Tools
Search
Changes
Start of topic |
Skip to actions
---+ Bicolano and MOBIUS base logic ---++ Bicolano [[http://en.wikipedia.org/wiki/Bikol_language][Bicolano]] (BYte COde LANguage in cOq) is concerned with the formalization of the Java Bytecode semantics with the [[http://coq.inria.fr/][Coq]] proof assistant. This page gathers the main files of the formal development. The whole bundle of Coq files can be [[%ATTACHURL%/bicolano_package.tgz][downloaded here]] and checked with [[http://coq.inria.fr/distrib-eng.html][Coq 8.0pl3]]. Html files are listed here: * Axiomatic definition of program syntax: [[%ATTACHURL%/Program.html][Program.v]] * Axiomatic definition of semantic domains: [[%ATTACHURL%/Domain.html][Domain.v]] * Axiomatic definition of machine arithmetic: [[%ATTACHURL%/Numeric.html][Numeric.v]] * Small step semantics: [[%ATTACHURL%/SmallStep.html][SmallStep.v]] * [[%ATTACHURL%/index.html][Global index]]. ---++ MOBIUS base logic MOBIUS base logic is the core program logic for bytecode and it relies on Bicolano JVM semantics. It is formalised with the [[http://coq.inria.fr/][Coq]] proof assistant. Its bundle with Coq files can be [[%ATTACHURL%/mbl_package.tgz][downloaded here]] and checked with [[http://coq.inria.fr/distrib-eng.html][Coq 8.0pl3]].
End of topic
Skip to action links
|
Back to top
r1.9 :
Edit
|
Attach image or document
|
Printable version
|
Raw text
|
Page history
|
More actions
You are here:
Bicolano
>
WebHome
to top
Ideas, requests, problems regarding the Mobius site