Incremental pattern-based coinduction for process algebra and its Isabelle formalization

Conference paper

Popescu, A. and Gunter, E. 2010. Incremental pattern-based coinduction for process algebra and its Isabelle formalization. Foundations of Software Science and Computation Structures (FOSSACS). Paphos, Cyprus 20 - 28 Mar 2010 Springer. pp. 109-127
TypeConference paper
TitleIncremental pattern-based coinduction for process algebra and its Isabelle formalization
AuthorsPopescu, A. and Gunter, E.
Abstract

We present a coinductive proof system for bisimilarity in
transition systems specifiable in the de Simone SOS format. Our coinduction is incremental, in that it allows building incrementally an a priori unknown bisimulation, and pattern-based, in that it works on equalities of process patterns (i.e., universally quantified equations of process terms containing process variables), thus taking advantage of equational reasoning in a “circular” manner, inside coinductive proof loops. The proof system has been formalized and proved sound in Isabelle/HOL

Research GroupFoundations of Computing group
ConferenceFoundations of Software Science and Computation Structures (FOSSACS)
Page range109-127
ISSN0302-9743
ISBN
Hardcover9783642120312
PublisherSpringer
Publication dates
Print2010
Publication process dates
Deposited27 Apr 2015
Output statusPublished
Copyright Statement

Access to full text restricted pending copyright check

LanguageEnglish
Book titleFoundations of Software Science and Computational Structures : 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/8520z

Log in to edit
File access - Request a copy

Restricted files

Accepted author manuscript

  • 17
    total views
  • 1
    total downloads
  • 2
    views this month
  • 0
    downloads this month

Export as