Quote: to understand an expression must know the data type of each variable in the expression [»browRE7_1976]

Quote: a type system is a set of rules for associating a type with every meaningful subexpression [»wegnP10_1986]

Quote: type-checking sees types as syntactic constraints that guarantees compatibility of composite expressions

Quote: Capability Language (CL) propagates capabilities for region-based memory operations; provably safe type system; lexical scope not required; e.g., extensible systems and continuation-passing style [»walkD7_2000]

Quote: Capability Language (CL), provably safe intermediate language for region-based memory management; supports aliasing and extensible OS; best for continuation-passing languages [»walkD7_2000]

Quote: associate capability and type with each object; guarantees exclusive ownership for deallocation or reuse; extends linear type systems [»walkD7_2000]

Quote: datatypes in ML by type constructors which represent the type and construct new instances of the type [»readC_1989]

Quote: every type in ML, including list constructors, can be defined in terms of tuple and function types; predefined types for efficiency [»readC_1989]

Quote: formalization of XML Schema using tree grammars; named types and structural types; matching and validation [»simeJ1_2003]

Quote: formalization of XML Schema used for XQuery and XPath specifications; one of the first

Quote: validation theorem -- validates iff matches and erases; roundtripping if unambiguous [»simeJ1_2003]

Quote: Kleisli and its self-describing data exchange use parametric polymorphism and type inference; from functional programming [»wongL9_2000]

Quote: define object types by arbitrarily nested records (f:t), sets {t}, bags {|t|}, lists [t], and variants ; natural mappings for bioinformatics databases [»wongL9_2000]

Quote: Kleisli uses the nested relational calculus (NRC); lambda calculus plus records, and sets [»wongL9_2000]

Quote: a function type is a cross product of its argument types to its result type [»kiebRB9_1973, OK]

Quote: many types do not have explicit names; e.g., operator or function types [»kiebRB9_1973]

Quote: a type algebra is intrinsically first-order; needs homeomorphisms from functions to relations [»reynJC9_1983]

Quote: in modern type theory, types are values in a suitable semantic domain; type constructors are maps from this domain into itself [»nelsG_1991]

Quote: in the theory of dependent types, Modula-3's generic interface is a function from module-values to module-types and a generic module is a function from module-values to module-values [»nelsG_1991]

Quote: an algebraic specification of an abstract type consists of its syntax (names, domains, ranges) and the relations of its operations [»guttJV6_1977]

Quote: type completeness--all data types enjoy equal status; e.g., Pascal functions cannot return arrays or functions [»atkiMP6_1987]

Quote: in a type-complete language, type of a name or expression can not depend on context

Quote: in a type-complete language, any expression can be parameterized with respect to any free name

Quote: type-complete language if type for every name, every expression or composite, independent of context, allowable types exist, parameterized expressions [»demeA_1980]

Quote: simplest type-complete language is the typed lambda calculus [»demeA_1980]

Quote: in a type-complete language, parameterization and application are universally applicable [»demeA_1980]

Quote: with type-completeness, any name that can be declared can also be a parameter [»demeA_1980]

QuoteRef: demeAJ_1980 ;; presentation of data types in Russell