Ulrich Berger, Helmut Schwichtenberg: An Inverse of the Evaluation Functional for Typed lambda-calculus. LICS 1991: 203-211