Mechanizing formal systems, given via axioms and inference rules,
together with proofs about them plays an important role in
establishing trust in formal developments. Over the past decade, the
POPLMark challenge popularized the use of proof assistants in
mechanizing the metatheory of programming languages. Focusing on the
the meta-theory of System F with subtyping, it allowed the programming
languages community to survey existing techniques to represent and
reason about syntactic structures with binders and promote the use of
proof assistants. Today, mechanizing proofs is a stable fixture in the
daily life of programming languages researchers. 

As a follow-up to the POPLMark Challenge, we propose a new collection of
benchmarks that use proofs by logical relations. Such proofs are now used to attack
problems in the theory of complex languages models, with applications
to issues in equivalence of programs, compiler correctness,
representation independence and even more intensional  properties such
as non-interference, differential privacy and secure multi-language
inter-operability. Yet, they remain challenging to mechanize.
 

In this talk, we focus on one particular challenge problem, namely
strong normalization of a simply-typed lambda-calculus with a proof by
Kripke-style logical relations. We will advocate a modern view of this
well-understood problem by formulating our logical relation on
well-typed terms.  Using this case study, we share some of the lessons
learned tackling this challenge problem in Beluga, a proof environment
that supports higher-order abstract syntax encodings, first-class
context and first-class substitutions. We also discuss and highlight
similarities, strategies, and limitations in other proof assistants
when tackling this challenge problem. 

We hope others will be motivated to submit solutions! The goal of this
talk is to engage the community in discussions on what support in
proof environments is needed to truly bring mechanized metatheory to
the masses.
