User loginNavigation 
Examples of Categorical Semantics for Languages with Dependent TypesIs 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 helpfulsystem 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 higherorder abstraction. But, I would like to describe the semantics of /\n.list(n). By echinuz at 20070906 20:43  LtU Forum  previous forum topic  next forum topic  other blogs  6049 reads

Browse archivesActive forum topics 
Recent comments
7 hours 27 min ago
8 hours 1 min ago
10 hours 13 min ago
10 hours 36 min ago
13 hours 55 min ago
15 hours 42 sec ago
18 hours 34 min ago
19 hours 13 min ago
1 day 7 hours ago
1 day 8 hours ago