logical-relations An exercise in using logical relations to prove strong normalization and semantic type safety for simply-typed lambda calculus.