POPLMark reloaded: Mechanizing proofs by logical relations