Roel C. de Vrijer: Big trees in a lambda - calculus with lambda - expressions as types. Lambda-Calculus and Computer Science Theory 1975: 252-271