A Case Study on Logical Relations using Contextual Types

TL;DR

This paper demonstrates a mechanized proof of algorithmic equality for simply typed lambda-terms using Beluga, highlighting the advantages of higher-order abstract syntax, recursive types, and Beluga's context support.

Contribution

It presents a novel, compact mechanization of logical relations proofs in Beluga, leveraging its features for encoding semantics and equivalence of lambda-terms.

Findings

Successful encoding of lambda-terms with operational semantics in Beluga

Effective use of recursive types and higher-order functions for logical equivalence

Demonstration of Beluga's capabilities in formalizing logical relations proofs

Abstract

Proofs by logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe the completeness 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 equality 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 simultaneous substitutions. This leads to a direct and compact mechanization, demonstrating Beluga's strength at formalizing logical relations proofs.