The Sage Programming Language

Overview

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.

Software

The current implementation is a type checker and interpreter for the Sage programming language. Any system with OCaml and GNU Make should be able to build Sage, and some of the support scripts require Perl and a reasonable unix scripting environment (Cygwin should work). Sage currently requires the Simplify theorem prover for hybrid type checking. The Sage code is licensed under the GPL, while Simplify is distributed under its own license, available here.

Download [zip] the current code snapshot. Note that this is a research prototype and a work in progress.

Documentation and Papers

Start with the tutorial and then move on to the papers below. Send comments and questions to sqt-sage@lists.dforge.cse.ucsc.edu

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.

Credits

The key developers of Sage are:
Cormac Flanagan (UCSC)
Steve Freund (Williams College)
Jessica Gronski (UCSC)
Kenn Knowles (UCSC)
Aaron Tomb (UCSC)
We additionally would like to thank Benjamin Pierce, whose sample code from Types and Programming Languages we used as a starting point.

From Wikipedia:

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?".