swMATH ID: 30073
Software Authors: Jessica Gronski , Kenneth Knowles , Aaron Tomb , Stephen N. Freund , Cormac Flanagan
Description: Sage: Hybrid checking for flexible specifications. Software systems typically contain large APIs that are informally specified and hence easily misused. This paper presents the Sage programming language, which is designed to enforce precise interface specifications in a flexible manner. The Sage type system uses a synthesis of the type Dynamic, first-class types, and arbitrary refinement types. Since type checking for this expressive language is not statically decidable, Sage uses hybrid type checking, which extends static type checking with dynamic contract checking, automatic theorem proving, and a database of refuted subtype judgments.
Homepage: http://dept.cs.williams.edu/~freund/papers/htc-sage.pdf
Related Software: gradualizerDynamicSemantics; Flow; PoplMark; Agda; Isabelle/HOL; Coq; Stabilizer; Thorn; Bigloo; Pycket; Python; LISP; JavaScript; Racket; PERL; Cecil; CLEAN
Cited in: 4 Documents

Citations by Year