Proof-rules for Certifying Memory Bounds
(by Javier de Dios and Ricardo Peña, January 2011)
Up
to index of Isabelle/HOL
View
theory dependencies
View
document
View
outline
Theories
SafeHeap
HaskellLib
SafeExpr
BinOP
SVMState
Lubs
GCD
Abstract_Rat
Rational
PReal
RealDef
RComplete
ContNotDenum
RealPow
RealVector
Real
SafeRASemanticsReal
SafeDepthSemanticsReal
Costes_definitions
CostesDepth
ProofRulesCostes