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: | , , |
| Format: | Article in Journal/Newspaper |
| Language: | English |
| Published: |
Cambridge University Press (CUP)
2018
|
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1017/s0960129518000415 https://www.cambridge.org/core/services/aop-cambridge-core/content/view/S0960129518000415 |