Concept: Abstract data type

A type-theoretic account of abstraction functions and cost verification

Using types to verify that software implementations match their abstract specifications