A Case Study on Logical Relations using Contextual Types
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2015-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1507.08053v1 |