A case study in programming coinductive proofs: Howe's method
Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the p...
Published in: | Mathematical Structures in Computer Science |
---|---|
Main Authors: | , , |
Other Authors: | , , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Cambridge University Press
2018
|
Subjects: | |
Online Access: | http://hdl.handle.net/2434/598000 https://doi.org/10.1017/S0960129518000415 |
id |
ftunivmilanoair:oai:air.unimi.it:2434/598000 |
---|---|
record_format |
openpolar |
spelling |
ftunivmilanoair:oai:air.unimi.it:2434/598000 2024-02-04T09:59:15+01:00 A case study in programming coinductive proofs: Howe's method MOMIGLIANO, ALBERTO PIENTKA, BRIGITTE THIBODEAU, DAVID A. Momigliano B. Pientka D. Thibodeau 2018-10-31 http://hdl.handle.net/2434/598000 https://doi.org/10.1017/S0960129518000415 eng eng Cambridge University Press info:eu-repo/semantics/altIdentifier/wos/WOS:000489561000012 firstpage:1 lastpage:35 numberofpages:35 journal:MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE http://hdl.handle.net/2434/598000 doi:10.1017/S0960129518000415 info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85056076324 info:eu-repo/semantics/openAccess Settore INF/01 - Informatica Settore MAT/01 - Logica Matematica info:eu-repo/semantics/article 2018 ftunivmilanoair https://doi.org/10.1017/S0960129518000415 2024-01-09T23:44:08Z Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe's method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga's support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga's reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga's strength at mechanizing challenging (co)inductive proofs using HOAS encodings. Article in Journal/Newspaper Beluga Beluga* The University of Milan: Archivio Istituzionale della Ricerca (AIR) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) Mathematical Structures in Computer Science 29 8 1309 1343 |
institution |
Open Polar |
collection |
The University of Milan: Archivio Istituzionale della Ricerca (AIR) |
op_collection_id |
ftunivmilanoair |
language |
English |
topic |
Settore INF/01 - Informatica Settore MAT/01 - Logica Matematica |
spellingShingle |
Settore INF/01 - Informatica Settore MAT/01 - Logica Matematica MOMIGLIANO, ALBERTO PIENTKA, BRIGITTE THIBODEAU, DAVID A case study in programming coinductive proofs: Howe's method |
topic_facet |
Settore INF/01 - Informatica Settore MAT/01 - Logica Matematica |
description |
Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe's method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga's support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga's reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga's strength at mechanizing challenging (co)inductive proofs using HOAS encodings. |
author2 |
A. Momigliano B. Pientka D. Thibodeau |
format |
Article in Journal/Newspaper |
author |
MOMIGLIANO, ALBERTO PIENTKA, BRIGITTE THIBODEAU, DAVID |
author_facet |
MOMIGLIANO, ALBERTO PIENTKA, BRIGITTE THIBODEAU, DAVID |
author_sort |
MOMIGLIANO, ALBERTO |
title |
A case study in programming coinductive proofs: Howe's method |
title_short |
A case study in programming coinductive proofs: Howe's method |
title_full |
A case study in programming coinductive proofs: Howe's method |
title_fullStr |
A case study in programming coinductive proofs: Howe's method |
title_full_unstemmed |
A case study in programming coinductive proofs: Howe's method |
title_sort |
case study in programming coinductive proofs: howe's method |
publisher |
Cambridge University Press |
publishDate |
2018 |
url |
http://hdl.handle.net/2434/598000 https://doi.org/10.1017/S0960129518000415 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_relation |
info:eu-repo/semantics/altIdentifier/wos/WOS:000489561000012 firstpage:1 lastpage:35 numberofpages:35 journal:MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE http://hdl.handle.net/2434/598000 doi:10.1017/S0960129518000415 info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85056076324 |
op_rights |
info:eu-repo/semantics/openAccess |
op_doi |
https://doi.org/10.1017/S0960129518000415 |
container_title |
Mathematical Structures in Computer Science |
container_volume |
29 |
container_issue |
8 |
container_start_page |
1309 |
op_container_end_page |
1343 |
_version_ |
1789963931100381184 |