Daniel Yoder wrote:
[...] are there any attempts to map category theory (or type theory or set theory -- I am not sure where the boundaries are)
to applications (versus theory per se), roughly analagous to Z or VDM, that might be comprehensible to somewhat without the formal framework? If not, is there a sequence of study you would recommend for proceeding?
Maybe you will find the following paper useful: D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, to appear (1997). Abstract: The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way. An attempt is made to offer an overall view, rather than new results, and to focus on the basic motivation behind the technicalities presented elsewhere. http://www.dcs.ed.ac.uk/home/dts/pub/concepts.{dvi,ps,pdf} The presentation is intended to be accessible to "ordinary" computer scientists. If you find the approach attractive and want to look at the technical details, follow the many references given in the paper (most of the papers by me are available electronically in http://www.dcs.ed.ac.uk/home/dts/pub/). These details are phrased in terms of simple concepts from category theory, universal algebra and logic. Regards, Don Sannella Univ. of Edinburgh dts@dcs.ed.ac.uk