typing-project Type checking for system F + GADTs and defunctionalization, a type-preserving program transformation. From the MPRI course "Functional programming and type systems".