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

Browse archivesActive forum topics 
Recent comments
15 hours 14 min ago
16 hours 13 min ago
1 day 9 hours ago
5 days 4 hours ago
5 days 9 hours ago
5 days 11 hours ago
5 days 22 hours ago
1 week 17 hours ago
1 week 2 days ago
1 week 2 days ago