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 2012-05-17 14:47 | LtU Forum | previous forum topic | next forum topic | other blogs | 8591 reads
|
Browse archivesActive forum topics |
Recent comments
7 weeks 2 days ago
7 weeks 4 days ago
7 weeks 5 days ago
14 weeks 5 days ago
20 weeks 3 days ago
20 weeks 4 days ago
21 weeks 3 days ago
24 weeks 1 day ago
25 weeks 4 days ago
25 weeks 5 days ago