Lambda the Ultimate

Is there a reference that describes how to define categorical semantics for lambda calculus enriched with dependent types? Both Pierce and Gunter give a good description of the categorical semantics of lambda calculus in their respective books. However, they use a simple type system. I would like to see a description of something more expressive. Examples from any class of dependent type system are helpful--system F, full calculus of constructions, etc...

I am working on a language where I would like to have simple dependent types such as sized lists. I don't really need higher-order abstraction. But, I would like to describe the semantics of /\n.list(n).

The web site description of CoScripter:

CoScripter is a system for recording, automating, and sharing processes performed in a web browser such as printing photos online, requesting a vacation hold for postal mail, or checking bank account information. Instructions for processes are recorded and stored in easy-to-read text here on the CoScripter web site, so anyone can make use of them. If you are having trouble with a web-based process, check to see if someone has written a CoScript for it!

Jon's discussion emphasizes the DSL perspective (and end-user programming).

The community dynamics enabled by exposing a DSL seem to me the interesting aspect of this discussion. Yet another example you can use when arguing in favor of textual, user accessible, DSLs.

From the 2005 ACM SIGPLAN Workshop on ML, here is An Applicative Control-Flow Graph Based on Huet's Zipper, by Norman Ramsey and João Dias.

We are using ML to build a compiler that does low-level optimization. To support optimizations in classic imperative style, we built a control-flow graph using mutable pointers and other mutable state in the nodes. This decision proved unfortunate: the mutable flow graph was big and complex, it led to many bugs. We have replaced it by a smaller, simpler, applicative flow graph based on Huet's (1997) zipper. The new flow graph is a success; this paper presents its design and shows how it leads to a gratifyingly simple implementation of the dataflow framework developed by Lerner, Grove, and Chambers (2002).