Keyword: normalization by evalution

• Tait: A normalization proof a la Tait for simply-typed lambda-calculus
  Helmut Schwichtenberg, Pierre Letouzey