Mechanizing proofs with logical relations – Kripke-style
Proofs with 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 two case studies using the proof environment Beluga : First, we explain the mechanization of the weak normali...
| Published in: | Mathematical Structures in Computer Science |
|---|---|
| Main Authors: | , |
| Format: | Article in Journal/Newspaper |
| Language: | English |
| Published: |
Cambridge University Press (CUP)
2018
|
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1017/s0960129518000154 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0960129518000154 |
| Summary: | Proofs with 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 two case studies using the proof environment Beluga : First, we explain the mechanization of the weak normalization proof for the simply typed lambda-calculus; second, we outline how to mechanize the completeness proof of algorithmic equality for simply typed lambda-terms where we reason about logically equivalent terms. The development of these proofs in Beluga relies on three key ingredients: (1) we encode lambda-terms together with their typing rules, operational semantics, algorithmic and declarative equality using higher order abstract syntax (HOAS) thereby avoiding the need to manipulate and deal with binders, renaming and substitutions, (2) we take advantage of Beluga 's support for representing derivations that depend on assumptions and first-class contexts to directly state inductive properties such as logical relations and inductive proofs, (3) we exploit Beluga 's rich equational theory for simultaneous substitutions; as a consequence, users do not need to establish and subsequently use substitution properties, and proofs are not cluttered with references to them. We believe these examples demonstrate that Beluga provides the right level of abstractions and primitives to mechanize challenging proofs using HOAS encodings. It also may serve as a valuable benchmark for other proof environments. |
|---|