Types and programming languages in REDEX Some formalizations of Pierce's book types and programming languages in PLT-Redex.