Concept: Formal verification

A type-theoretic account of abstraction functions and cost verification

Using types to verify that software implementations match their abstract specifications