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

6 weeks 6 days ago

7 weeks 1 day ago

7 weeks 2 days ago

14 weeks 2 days ago

20 weeks 15 hours ago

20 weeks 1 day ago

21 weeks 16 hours ago

23 weeks 6 days ago

25 weeks 1 day ago

25 weeks 2 days ago