Certified Absence of Dangling Pointers
(by Javier de Dios and Ricardo Peña, July 2010)
Up
to index of Isabelle/HOL
View
theory dependencies
View
document
View
outline
Theories
TypeEnvironment
SafeHeap
HaskellLib
SafeExpr
BinOP
SVMState
SafeRASemantics
SafeDepthSemantics
ClosureHeap
SafeDAssBasic
SafeDAss_P2
SafeDAss_P3
SafeDAss_P1
SafeRegion_definitions
BasicFacts
SafeDAss_P5_P6
SafeDAss_P4
SafeDAss_P7
SafeDAss_P8
SafeDAss_P9
SafeDAssDepth
ProofRules
SafeRegionDepth
ProofRulesRegions