Sage: Practical Hybrid Type Checking
Kenn Knowles
- Place: E2, Rm 392
- Time: 2-3:10pm, Wednesday, January 25, 2006
Abstract
The Sage programming language supports precise specifications through a dependent type system in which types may be refined to uphold arbitrary predicates. To enforce these expressive specifications, Sage uses hybrid type checking, which integrates static type checking, dynamic contract checking, and automatic theorem proving techniques. Experimental results show that Sage can verify many correctness properties at compile time, and can detect more defects than traditional static type systems.