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

Browse archives
Active forum topics 
Recent comments
4 days 4 hours ago
4 days 14 hours ago
1 week 11 hours ago
1 week 1 day ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
2 weeks 5 days ago
3 weeks 4 days ago