A Case Study on Logical Relations using Contextual Types
Andrew Cave (McGill University), Brigitte Pientka (McGill University)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Semantic Web and Ontologies · Logic, Reasoning, and Knowledge
