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.