λ☶ (pronounced Lambda Mountain) is a compiler backend that provides a relatively clean implementation of System F<: with Specialization. The whole compiler is only 5000 lines of code.