Abstract

The worklist style inference algorithm is marvelous legacy left by no other than the great Dr. Jimmy Zhao, which handles the problem of type inference for a system with higher-ranked polymorphism efficiently and elegantly. In this seminar we are going to explore what would happen when we attempt to generalize the algorithm to a dependently-typed system. And see if the method still holds its former glory.