The Sage Programming Language
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.
Download [zip] the current code snapshot. Note that this is a research prototype and a work in progress.
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic . Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N. Freund, Cormac Flanagan. Revised and extended version of our paper at the 2006 Scheme and Functional Programming workshop.
Compositional and Decidable Checking for Dependent Contract Types. Kenneth Knowles, Cormac Flanagan. Tech Report UCSC-SOE-08-17 2008.
Space Efficient Gradual Typing. Dave Herman, Aaron Tomb, Cormac Flanagan. TFP 2007.
Unifying Hybrid Types and Contracts. Jessica Gronski, Cormac Flanagan. TFP 2007.
Type Reconstruction for General Refinement Types. Kenneth Knowles, Cormac Flanagan. ESOP 2007. (extended version)
Hybrid Types, Invariants, and Refinements for Imperative Objects. Cormac Flanagan, Stephen N. Freund, and Aaron Tomb. FOOL 2006.
Hybrid Type Checking. Cormac Flanagan. POPL 2006.
Cormac Flanagan (UCSC)We additionally would like to thank Benjamin Pierce, whose sample code from Types and Programming Languages we used as a starting point.
Steve Freund (Williams College)
Jessica Gronski (UCSC)
Kenn Knowles (UCSC)
Aaron Tomb (UCSC)
Sage is a term used for plants of the genus Salvia... The name Salvia derives from the Latin 'salveo', which means 'to heal'. Indeed this herb is highly regarded for its healing qualities. An ancient proverb states, "Why should a man die who has sage in his garden?".