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 |
id |
crcambridgeupr:10.1017/s0960129518000154 |
---|---|
record_format |
openpolar |
spelling |
crcambridgeupr:10.1017/s0960129518000154 2024-03-03T08:43:10+00:00 Mechanizing proofs with logical relations – Kripke-style CAVE, ANDREW PIENTKA, BRIGITTE 2018 http://dx.doi.org/10.1017/s0960129518000154 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0960129518000154 en eng Cambridge University Press (CUP) https://www.cambridge.org/core/terms Mathematical Structures in Computer Science volume 28, issue 9, page 1606-1638 ISSN 0960-1295 1469-8072 Computer Science Applications Mathematics (miscellaneous) journal-article 2018 crcambridgeupr https://doi.org/10.1017/s0960129518000154 2024-02-08T08:29:56Z 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. Article in Journal/Newspaper Beluga Beluga* Cambridge University Press Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) Mathematical Structures in Computer Science 28 9 1606 1638 |
institution |
Open Polar |
collection |
Cambridge University Press |
op_collection_id |
crcambridgeupr |
language |
English |
topic |
Computer Science Applications Mathematics (miscellaneous) |
spellingShingle |
Computer Science Applications Mathematics (miscellaneous) CAVE, ANDREW PIENTKA, BRIGITTE Mechanizing proofs with logical relations – Kripke-style |
topic_facet |
Computer Science Applications Mathematics (miscellaneous) |
description |
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. |
format |
Article in Journal/Newspaper |
author |
CAVE, ANDREW PIENTKA, BRIGITTE |
author_facet |
CAVE, ANDREW PIENTKA, BRIGITTE |
author_sort |
CAVE, ANDREW |
title |
Mechanizing proofs with logical relations – Kripke-style |
title_short |
Mechanizing proofs with logical relations – Kripke-style |
title_full |
Mechanizing proofs with logical relations – Kripke-style |
title_fullStr |
Mechanizing proofs with logical relations – Kripke-style |
title_full_unstemmed |
Mechanizing proofs with logical relations – Kripke-style |
title_sort |
mechanizing proofs with logical relations – kripke-style |
publisher |
Cambridge University Press (CUP) |
publishDate |
2018 |
url |
http://dx.doi.org/10.1017/s0960129518000154 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0960129518000154 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
Mathematical Structures in Computer Science volume 28, issue 9, page 1606-1638 ISSN 0960-1295 1469-8072 |
op_rights |
https://www.cambridge.org/core/terms |
op_doi |
https://doi.org/10.1017/s0960129518000154 |
container_title |
Mathematical Structures in Computer Science |
container_volume |
28 |
container_issue |
9 |
container_start_page |
1606 |
op_container_end_page |
1638 |
_version_ |
1792498592942915584 |