Develop and extend the concepts of sketch and categorical theory as a tool for the specification and precise description of data types and the syntax and semantics of computer languages. The sketch gives a formal finite specification of a data type or language construct, or of a whole language. Categorical semantics includes: initial algebra semantics, greatly generalizing the work of Goguen; the categorical theory generated by the sketch, which encapsulates the whole language implied by a sketched specification; and models in the categorical sense as functors. Specific tasks will include: (a) Using FS sketches with multiple initial algebras as models for data types with overflow. (b) Using sketches to specify a functional programming language, which will involve understanding (c) the correct place in the hierarchy of types of sketches and theories for such descriptions, and (d) the correct abstract semantics and its connection with computable semantics. (e) Understand how the recursive definition of data types can be sketched. (f) Understand the way functions as first class objects and the resulting cartesian closed category interacts with the use of sketched specifications and with the semantics. (g) Formulate the correct definition of "environment" in this context. (h) Analyze an existing functional programming language using these techniques. (i) Develop a prototype implementation of a categorical computer language.
