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.
Recent comments
3 hours 57 min ago
5 hours 16 min ago
5 hours 38 min ago
9 hours 9 min ago
15 hours 1 min ago
15 hours 8 min ago
17 hours 2 min ago
1 day 2 hours ago
1 day 22 hours ago
2 days 8 hours ago