A case study in programming coinductive proofs: Howe's method

• Published in: Mathematical Structures in Computer Science
• Main Authors: MOMIGLIANO, ALBERTO, PIENTKA, BRIGITTE, THIBODEAU, DAVID
• Other Authors: A. Momigliano, B. Pientka, D. Thibodeau
• Format: Article in Journal/Newspaper
• Language: English
• Published: Cambridge University Press 2018
• Subjects: Settore INF/01 - Informatica; Settore MAT/01 - Logica Matematica; Lambda; Beluga; Beluga*
• Online Access: http://hdl.handle.net/2434/598000; https://doi.org/10.1017/S0960129518000415

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...