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

Browse archivesActive forum topics 
Recent comments
1 day 6 hours ago
1 day 20 hours ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 6 days ago
2 weeks 6 days ago
2 weeks 6 days ago
2 weeks 6 days ago
3 weeks 1 day ago
3 weeks 2 days ago