From: cat-dist@mta.ca [mailto:cat-dist@mta.ca] On Behalf Of Michael Barr Sent: Friday, January 04, 2002 10:04 AM I call your attention to the web site http://www.haskell.org/bookshelf/ What I found especially interesting was the last section (Foundations) of this page. Yes, category theory is now used fairly commonly in the separate but closely related fields of programming language semantics and functional programming. While we are citing references, here is one that I think pure mathematicians would find interesting: Richard Bird and Oege de Moor, Algebra of Programming, Prentice-Hall, 1997. Bird and De Moor apply algebras, coalgebras, and allegories to small-scale programming problems. See also the many papers by Lambert Meertens, who is one of the founders of this approach to "calculational programming". On the topic of programming languages, I would like to direct categorical logicians' attention to Lego, Cayenne, and Agda (and perhaps others). These languages implement Martin-Lof type theory with a universe hierarchy and are interesting because they combine programming language, proof system, and module system into a single type theory. Since these three functionalities are typically separate in most programming languages, combining them yields a significant three-for-one economy. Also, unlike most programming languages, these languages include dependent sums and products, which are used pervasively in standard mathematics. Indeed, it seems to me that Martin-Lof type theory closely achieves (one of) its original aims of modeling informal mathematical practice. The last chapter of Bart Jacobs, Categorical Logic and Type Theory, Elsevier, 1999. covers the categorical logic of this type theory but doesn't describe the universe hierarchy in detail (see page 691). Is there any work showing how to model a universe hierarchy categorically? I'm sure it would be clear if I really understood Jacobs, but that's a big if. And I am sure that many programming language researchers would appreciate a more tutorial presentation of the semantics of this type theory than appears in Jacobs' book. Andy Pitts and Martin Hoffman have some tutorial papers, but, in this case, more is better. David