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

Browse archivesActive forum topics 
Recent comments
4 days 22 hours ago
1 week 1 hour ago
1 week 2 hours ago
1 week 2 hours ago
1 week 3 hours ago
1 week 3 hours ago
1 week 5 hours ago
1 week 9 hours ago
1 week 11 hours ago
1 week 15 hours ago