QuoteRef: kiebRB9_1973 ;;%Earley: pointer in a data structure is an access path

1.1 ;;Quote: data structures become references to variables, array elements, and pointers

QuoteRef: kiebRB9_1973 ;;1.1 separates data declarations for data implementation

QuoteRef: kiebRB9_1973 ;;1.1 separates definition of data structures from their use for proving

QuoteRef: kiebRB9_1973 ;;1.2 separates "type declaration from the semantic definition of a type

2.1 ;;Quote: a type is a predicate defining a class of interpretations of abstract objects

QuoteRef: kiebRB9_1973 ;;2.2 reference to a var produces an object of that type (eg ->real)

QuoteRef: kiebRB9_1973 ;;2.2 "Composite types are formed from simple types and from the symbol ->, used to indicate a reduction rule, or function on types." parens are used to indicate scope

QuoteRef: kiebRB9_1973 ;;2.3 "Arrays of scalar variables are formed by using type functions with arguments of type i (%integer)." e.g., ->(->real) is a one dim. array and iXi->(->real) is a two dim. array

2.3 ;;Quote: an operator can have a polymorphic type, i.e., a union of signatures with different operand types

2.3 ;;Quote: a function type is a cross product of its argument types to its result type

2.4 ;;Quote: some values of composite types are invalid; need run-time checks, e.g., array bounds

QuoteRef: kiebRB9_1973 ;;2.4 user defined types may be given names and grouped into records eg list element by L: ((-> r), (-> L))

QuoteRef: kiebRB9_1973 ;;2.4 "...the name of a type cannot appear as a field of its own declaration eg L:((->r),L)

QuoteRef: kiebRB9_1973 ;;4.2 parameterized type eg P(x): -> allows pointer to any named type

4.2 ;;Quote: many types do not have explicit names; e.g., operator or function types

QuoteRef: kiebRB9_1973 ;;4.3 extend syntax eg expression ::= identifier of expression for access

QuoteRef: kiebRB9_1973 ;;4.3 p(n) father of p(n) has composite type of p(n)->p(n) where p(n) is a pointer to a note (this forms a function returning type p(n))

QuoteRef: kiebRB9_1973 ;;4.4 declaration by match on pattern in class definition (unimplemented)

5.2 ;;Quote: use macros for operations in the representation type

QuoteRef: kiebRB9_1973 ;;6.2 proves program by formal properties expressed in representation type