Concept: Data type
FLAT uses formal languages to type strings
Using formal languages as type constraints to prevent string-based security vulnerabilities
A type-theoretic account of abstraction functions and cost verification
Using types to verify that software implementations match their abstract specifications
