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  5902 reads

Browse archivesActive forum topics 
Recent comments
15 hours 23 min ago
17 hours 31 min ago
1 day 46 min ago
1 day 5 hours ago
1 day 5 hours ago
1 day 8 hours ago
1 day 14 hours ago
1 day 16 hours ago
1 day 19 hours ago
1 day 19 hours ago