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

DOI10.1017/S0960129518000415zbMath1430.68418WikidataQ113857439 ScholiaQ113857439MaRDI QIDQ5236557

Brigitte Pientka, Alberto Momigliano, David Thibodeau

Publication date: 9 October 2019

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• HYBRID
• Beluga
• Twelf
• Bedwyr
• Abella
• Psi-calculi