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

Registo completo
Campo DCValorIdioma
dc.contributor.authorBarbosa, L. S.-
dc.contributor.authorOliveira, José Nuno Fonseca-
dc.contributor.authorSilva, Alexandra-
dc.date.accessioned2012-09-17T10:02:42Z-
dc.date.available2012-09-17T10:02:42Z-
dc.date.issued2008-
dc.identifier.isbn9783540799795por
dc.identifier.issn0302-9743-
dc.identifier.urihttps://hdl.handle.net/1822/20217-
dc.description.abstractInvariants, 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.por
dc.description.sponsorshipPartially supported by the Fundacao para a Ciencia e a Tecnologia, Portugal, under grant number SFRH/BD/27482/2006.por
dc.language.isoengpor
dc.publisherSpringerpor
dc.rightsopenAccesspor
dc.subjectCoalgebraic reasoningpor
dc.subjectProgram calculationpor
dc.subjectInvariantspor
dc.subjectproof obligationspor
dc.subjectpointfree transformpor
dc.titleCalculating invariants as coreflexive bisimulationspor
dc.typeconferencePaperpor
dc.peerreviewedyespor
sdum.publicationstatuspublishedpor
oaire.citationStartPage83por
oaire.citationEndPage99por
oaire.citationTitleLecture Notes in Computer Sciencepor
oaire.citationVolume5140por
dc.identifier.doi10.1007/978-3-540-79980-1_7por
dc.subject.wosScience & Technologypor
sdum.journalLecture Notes in Computer Sciencepor
sdum.conferencePublicationALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGSpor
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 ORCID