Edinburgh Research Explorer

Using a generalisation critic to find bisimulations for coinductive proofs

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Documents

Original languageEnglish
Title of host publicationAutomated Deduction—CADE-14
Subtitle of host publication14th International Conference on Automated Deduction Townsville, North Queensland, Australia, July 13–17, 1997 Proceedings
PublisherSpringer-Verlag GmbH
Pages276-290
ISBN (Electronic)978-3-540-69140-2
ISBN (Print)978-3-540-63104-0
DOIs
StatePublished - 1997

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume1249
ISSN (Print)0302-9743

Abstract

Coinduction is a method of growing importance in reasoning about functional languages, due to the increasing prominence of lazy data structures. Through the use of bisimulations and proofs that bisimilarity is a congruence in various domains it can be used to prove the congruence of two processes.
A coinductive proof requires a relation to be chosen which can be proved to be a bisimulation. We use proof planning to develop a heuristic method which automatically constructs a candidate relation. If this relation does not allow the proof to go through a proof critic analyses the reasons why it failed and modifies the relation accordingly.
Several proof tools have been developed to aid coinductive proofs but all require user interaction. Crucially they require the user to supply an appropriate relation which the system can then prove to be a bisimulation.

    Research areas

  • coinduction, proof planning, proof critics

Download statistics

No data available

ID: 6329542