10: {v : (IO ()) | v == Main.main}main = [Char] -> (IO ())putStrLn {v : [Char] | len v >= 0}"Easter Egg: to force Makefile"
Use Types to lift Logic + Analysis to Modern Programs
Take Home: Types are a simple and uniform way to analyze
Take Home 2: Uninterpreted Functions
Measures for Datatype properties
Abstract Refinements
Technology
Applications
http://goto.ucsd.edu/liquid