Abstract

Higher-order polymorphic type system is difficult to formalize in proof assistants. Recently we make use of the worklist judgment chain together with “cascading contexts” to eliminate the output context for such algorithms. However, during the proof development, some difficulties are found on the metatheory. I will briefly go through the algorithm again, and show differences between the cascading context and traditional contexts.