This work is licensed under the Creative Commons Attribution License. A Case Study on Logical Relations using Contextual Types

Proofs by logical relations play a key role to establish rich properties such as normalization or con-textual equivalence. They are also challenging to mechanize. In this paper, we describe the complete-ness proof of algorithmic equality for simply typed lambda-terms by Crary where we reason about logically equivalent terms in the proof environment Beluga. There are three key aspects we rely upon: 1) we encode lambda-terms together with their operational semantics and algorithmic equal-ity using higher-order abstract syntax 2) we directly encode the corresponding logical equivalence of well-typed lambda-terms using recursive types and higher-order functions 3) we exploit Beluga’s support for contexts and the equational theory of simultanous substitutions. This leads to a direct and compact mechanization, demonstrating Beluga’s strength at formalizing logical relations proofs.