POPLMark reloaded: Mechanizing proofs by logical relations
Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a...
Published in: | Journal of Functional Programming |
---|---|
Main Authors: | , , , , , , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Cambridge University Press (CUP)
2019
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1017/s0956796819000170 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796819000170 |
id |
crcambridgeupr:10.1017/s0956796819000170 |
---|---|
record_format |
openpolar |
spelling |
crcambridgeupr:10.1017/s0956796819000170 2024-09-15T17:59:02+00:00 POPLMark reloaded: Mechanizing proofs by logical relations ABEL, ANDREAS ALLAIS, GUILLAUME HAMEER, ALIYA PIENTKA, BRIGITTE MOMIGLIANO, ALBERTO SCHÄFER, STEVEN STARK, KATHRIN 2019 http://dx.doi.org/10.1017/s0956796819000170 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796819000170 en eng Cambridge University Press (CUP) https://www.cambridge.org/core/terms Journal of Functional Programming volume 29 ISSN 0956-7968 1469-7653 journal-article 2019 crcambridgeupr https://doi.org/10.1017/s0956796819000170 2024-09-04T04:04:45Z Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks. Article in Journal/Newspaper Beluga Beluga* Cambridge University Press Journal of Functional Programming 29 |
institution |
Open Polar |
collection |
Cambridge University Press |
op_collection_id |
crcambridgeupr |
language |
English |
description |
Abstract We propose a new collection of benchmark problems in mechanizing the metatheory of programming languages, in order to compare and push the state of the art of proof assistants. In particular, we focus on proofs using logical relations (LRs) and propose establishing strong normalization of a simply typed calculus with a proof by Kripke-style LRs as a benchmark. We give a modern view of this well-understood problem by formulating our LR on well-typed terms. Using this case study, we share some of the lessons learned tackling this problem in different dependently typed proof environments. In particular, we consider the mechanization in Beluga, a proof environment that supports higher-order abstract syntax encodings and contrast it to the development and strategies used in general-purpose proof assistants such as Coq and Agda. The goal of this paper is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses and engage said community in the crafting of future benchmarks. |
format |
Article in Journal/Newspaper |
author |
ABEL, ANDREAS ALLAIS, GUILLAUME HAMEER, ALIYA PIENTKA, BRIGITTE MOMIGLIANO, ALBERTO SCHÄFER, STEVEN STARK, KATHRIN |
spellingShingle |
ABEL, ANDREAS ALLAIS, GUILLAUME HAMEER, ALIYA PIENTKA, BRIGITTE MOMIGLIANO, ALBERTO SCHÄFER, STEVEN STARK, KATHRIN POPLMark reloaded: Mechanizing proofs by logical relations |
author_facet |
ABEL, ANDREAS ALLAIS, GUILLAUME HAMEER, ALIYA PIENTKA, BRIGITTE MOMIGLIANO, ALBERTO SCHÄFER, STEVEN STARK, KATHRIN |
author_sort |
ABEL, ANDREAS |
title |
POPLMark reloaded: Mechanizing proofs by logical relations |
title_short |
POPLMark reloaded: Mechanizing proofs by logical relations |
title_full |
POPLMark reloaded: Mechanizing proofs by logical relations |
title_fullStr |
POPLMark reloaded: Mechanizing proofs by logical relations |
title_full_unstemmed |
POPLMark reloaded: Mechanizing proofs by logical relations |
title_sort |
poplmark reloaded: mechanizing proofs by logical relations |
publisher |
Cambridge University Press (CUP) |
publishDate |
2019 |
url |
http://dx.doi.org/10.1017/s0956796819000170 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0956796819000170 |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
Journal of Functional Programming volume 29 ISSN 0956-7968 1469-7653 |
op_rights |
https://www.cambridge.org/core/terms |
op_doi |
https://doi.org/10.1017/s0956796819000170 |
container_title |
Journal of Functional Programming |
container_volume |
29 |
_version_ |
1810435979758010368 |