In this seminar we are going to explore the design choices of mechanised formalisation for type inference in a dependently type system with the idea of “worklist”. We use a simplified type system very close to the Calculus of Construction (or a specific Pure Type System) to hopefully minimize the noise and complications brought by the more advanced type system feature like (unified) subtyping, and illustrate the core formalisation routine of dependent type inference with worklist.