A normalization by evaluation algorithm for an intrinsically typed simply-typed lambda calculus.