Lambda the Ultimate

This research workshop takes place in Israel, so I doubt many of you will come, but the program is quite interesting so you might want to google some of the titles...

Since we've been discussing hybrid type checking, dependent types, etc. recently...

Sage

Sage is a prototype functional programming language designed to provide high-coverage checking of expressive program specifications (types). Sage allows a programmer to specify not only simple types such as "Integers" and "Strings" but also arbitrary refinements from simple ranges such as "Positive Integers" to data structures with complex invariants such as "Balanced binary search trees." In addition to featuring these predicates upon types, Sage merges the syntactic categories of types and terms, in the spirit of Pure Type Systems, to express dependent types such as that of the infamous printf function.

Sage performs hybrid type checking of these specifications, proving or refuting as much as possible statically, and inserting runtime checks otherwise. For the complete details of the theory and empirical results, we direct you to the technical report.