Coq formalization and implementation of the Fi+ calculus
Haskell implementation of Gradually Polymorphic Calculus
Coq formalization of a coherent calculus with records and disjoint intersection types that supports nested composition
Haskell implementation of a type system for first-class traits
Research middleware compiler from System F-based languages to Java with the Imperative Functional Object encoding