A Case Study on Logical Relations using Contextual Types

Andrew Cave
(McGill University)
Brigitte Pientka
(McGill University)

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.

In Iliano Cervesato and Kaustuv Chaudhuri: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP 2015), Berlin, Germany, 1 August 2015, Electronic Proceedings in Theoretical Computer Science 185, pp. 33–45.
Published: 27th July 2015.

ArXived at: https://dx.doi.org/10.4204/EPTCS.185.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org