Sage swMATH ID: 30073 Software Authors: Gronski, Jessica; Knowles, Kenneth; Tomb, Aaron; Freund, Stephen N.; Flanagan, Cormac 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: TreatJS; MoCHi; Forsythe; Stardust; Eiffel; LiquidHaskell; CDuce; TypeScript; gradualizerDynamicSemantics; Flow; PoplMark; Agda; Isabelle/HOL; Coq; Stabilizer; Thorn; Bigloo; Pycket; Python; LISP Cited in: 5 Documents all top 5 Cited by 16 Authors 2 Findler, Robert Bruce 2 Siek, Jeremy G. 1 Ahmed, Amal 1 Chen, Tianyu 1 Felleisen, Matthias 1 Feltey, Daniel 1 Flanagan, Cormac 1 Greenman, Ben 1 Herman, David 1 Igarashi, Atsushi 1 New, Max S. 1 Nishida, Yuki 1 Takikawa, Asumu 1 Tomb, Aaron 1 Vitek, Jan 1 Wadler, Philip Lee Cited in 2 Serials 2 Journal of Functional Programming 1 Higher-Order and Symbolic Computation Cited in 2 Fields 5 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) Citations by Year