Utilize este identificador para referenciar este registo: http://hdl.handle.net/1822/20217

TítuloCalculating invariants as coreflexive bisimulations
Autor(es)Barbosa, L. S.
Oliveira, José Nuno Fonseca
Silva, Alexandra
Palavras-chaveCoalgebraic reasoning
Program calculation
proof obligations
pointfree transform
RevistaLecture Notes in Computer Science
Resumo(s)Invariants, bisimulations and assertions are the main ingredients of coalgebra theory applied to software systems. In this paper we reduce the first to a particular case of the second and show how both together pave the way to a theory of coalgebras which regards invariant predicates as types. An outcome of such a theory is a calculus of invariants’ proof obligation discharge, a fragment of which is presented in the paper. The approach has two main ingredients: one is that of adopting relations as “first class citizens” in a pointfree reasoning style; the other lies on a synergy found between a relational construct, Reynolds’ relation on functions involved in the abstraction theorem on parametric polymorphism and the coalgebraic account of bisimulations and invariants. This leads to an elegant proof of the equivalence between two different definitions of bisimulation found in coalgebra literature (due to B. Jacobs and Aczel & Mendler, respectively) and to their instantiation to the classical Park-Milner definition popular in process algebra.
Arbitragem científicayes
Aparece nas coleções:HASLab - Artigos em revistas internacionais
DI/CCTC - Artigos (papers)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
AMAST08-BOS.pdfpreprint522,25 kBAdobe PDFVer/Abrir

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu Currículo DeGóis