Abstract

Giving a set of declarative typing rules for a type system is relatively easy, but giving a decidable algorithm is not. In this talk, I will introduce some work I have done about giving a bi-directional algorithmic typing rule for dependent types, with explicit type-level computation (casts) and let-generalization. The work is mainly inspired by the paper “Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism” (chosen as paper reading previously).