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 con-textual 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 lo...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
2007
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.722.3129 http://cs.mcgill.ca/%7Ebpientka/papers/logrel.pdf |
| Summary: | Proofs by logical relations play a key role to establish rich properties such as normalization or con-textual 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 simultanous substitutions. This leads to a direct and compact mechanization, demonstrating Beluga’s strength at formalizing logical relations proofs. |
|---|