typed-lambdaFactor a typed version of lambda-calculus with factorisation that supports self-interpretation