We give a short description of Hybrid, a new tool for interactive theorem proving. 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 lambda-calculus. In particular, we prove that the standard notion of simulation is a precongruence. Although such a proof is not new, 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.
A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity / A. Momigliano, S. Ambler, R. L. Crole. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 70:2(2002), pp. 60-75.
|Titolo:||A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity|
MOMIGLIANO, ALBERTO (Primo)
|Settore Scientifico Disciplinare:||Settore INF/01 - Informatica|
Settore MAT/01 - Logica Matematica
|Data di pubblicazione:||2002|
|Digital Object Identifier (DOI):||http://dx.doi.org/10.1016/S1571-0661(04)80506-1|
|Appare nelle tipologie:||01 - Articolo su periodico|