User loginNavigation |
archivesHow to write your next POPL paper in CoqIf this sounds like a worthy goal, or if you are simply interested in the use of proof assistants for rogramming language research, you don't want to miss upcoming tutorial. Weak normalisation theorem for typed lambda-calculusHi, There is something that seems strange to me. It says that: The degree &(T) of a type is defined by: The degree &(r) of a redex is defined by: Reading this it seems to me that a redex has the degree of its type. Am I wrong? Anyway, after it says: Note that, if r is a redex of type T, then &(r) > &(T). Why should &(r) be greater than &(T)? thanks, |
Browse archivesActive forum topics |
Recent comments
16 weeks 2 days ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 17 hours ago
51 weeks 5 days ago
51 weeks 5 days ago