Tag: Logic, programming, and type systems

A type-theoretic account of abstraction functions and cost verification

Using types to verify that software implementations match their abstract specifications