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: | Text |
| Language: | unknown |
| Published: |
arXiv
2015
|
| Subjects: | |
| Online Access: | https://dx.doi.org/10.48550/arxiv.1507.08053 https://arxiv.org/abs/1507.08053 |