User loginNavigation 
Encoding System Fw in predicative dependent type theorySystem F_{ω} appears impredicative, but I'm wondering if there is an easy way to embed it into predicative dependent type theory by inferring bounds on universes. Also, if anyone can provide an example of a System F_{ω} term that would be rejected by Coq's typical ambiguity resolver, that would be helpful to me. Any references or thought are appreciated. By Matt M at 20120517 14:47  LtU Forum  previous forum topic  next forum topic  other blogs  7523 reads

Browse archivesActive forum topics 
Recent comments
18 hours 31 min ago
1 day 26 min ago
1 day 2 hours ago
1 day 12 hours ago
3 days 7 hours ago
4 days 15 hours ago
4 days 15 hours ago
6 days 12 hours ago
1 week 26 min ago
1 week 2 days ago