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 log...