X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Fmatita%2Flibrary.shtml;h=c22db5e1ce9f03802dcbcb812811ff85175bef68;hb=2fbef023cc9fdb3d6982194ba62552a0605f2571;hp=6617949a5ebca6ca049d24e165402d2be6d403ca;hpb=e999e3e921dd6a7d2ef78e458bfbb26bdeaa4e7a;p=helm.git diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml index 6617949a5..c22db5e1c 100644 --- a/helm/www/matita/library.shtml +++ b/helm/www/matita/library.shtml @@ -1,6 +1,6 @@ - - + +
+ The scripts present: +
+ +The execution in the executable formalization has been compared + to real world execution using the USB SPYDER08 + in-circuit debugger. +
+ ++ The code (in OCaml) + of an executable emulator, + automatically generated from the scripts above. On the tests above, + it runs at about 29% of the speed of the + CodeWarrior + emulation engine. +
+ +The formalization has been the Undergraduate Thesis of + Mr. Cosimo Oliboni. The manuscript (italian only) can be found + + here. +
+ ++ See the λδ home page. +
+