Isabelle/HOL theories for Certification of the CoreSafe to SafeImp translation
(by Javier de Dios and Ricardo Peña, March 2009)
Up
to index of Isabelle/HOL
View
theory dependencies
View
document
View
outline
Theories
SafeHeap
HaskellLib
SafeExpr
BinOP
SVMState
SafeRASemantics
SVMSemantics
CoreSafeToSVM
CertifSafeToSVM_definitions
basic_properties
execSVMBalanced_lemmas
diff_lemmas
maxFreshCells_lemmas
maxFreshWords_lemmas
identityEnvironment_lemmas
CertifSafeToSVM