A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity

We give a short description of Hybrid, a new tool for interactive theorem proving, s introduced in [4]. It provides a form of Higher Order Abstract Syntax (HOAS) combined consistently with induction and coinduction. We present a case study illustrating the use of Hybrid for reasoning about the lazy -calculus. In particular, we prove that the standard notion of simulation is a precongruence. Although such a proof is not new [5], the development is non-trivial, and we attempt to illustrate the advantages of using Hybrid, as well as some issues which are being addressed as further work.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Alberto Momigliano, Simon Ambler, Roy L. Crole
• Keywords: Case Study, ENTCS 2002, Interactive Theorem, Short Description