A Case Study on Logical Relations using Contextual Types

• Published in: Electronic Proceedings in Theoretical Computer Science
• Main Authors: Andrew Cave, Brigitte Pientka
• Format: Article in Journal/Newspaper
• Language: English
• Published: Open Publishing Association 2015
• Subjects: Mathematics; QA1-939; Electronic computers. Computer science; QA75.5-76.95; Lambda; Beluga; Beluga*
• Online Access: https://doi.org/10.4204/EPTCS.185.3; https://doaj.org/article/a3349533a8984de8b01a2d13bd51a81a

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.