Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/20217
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Barbosa, L. S. | - |
dc.contributor.author | Oliveira, José Nuno Fonseca | - |
dc.contributor.author | Silva, Alexandra | - |
dc.date.accessioned | 2012-09-17T10:02:42Z | - |
dc.date.available | 2012-09-17T10:02:42Z | - |
dc.date.issued | 2008 | - |
dc.identifier.isbn | 9783540799795 | por |
dc.identifier.issn | 0302-9743 | - |
dc.identifier.uri | https://hdl.handle.net/1822/20217 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | Partially supported by the Fundacao para a Ciencia e a Tecnologia, Portugal, under grant number SFRH/BD/27482/2006. | por |
dc.language.iso | eng | por |
dc.publisher | Springer | por |
dc.rights | openAccess | por |
dc.subject | Coalgebraic reasoning | por |
dc.subject | Program calculation | por |
dc.subject | Invariants | por |
dc.subject | proof obligations | por |
dc.subject | pointfree transform | por |
dc.title | Calculating invariants as coreflexive bisimulations | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
sdum.publicationstatus | published | por |
oaire.citationStartPage | 83 | por |
oaire.citationEndPage | 99 | por |
oaire.citationTitle | Lecture Notes in Computer Science | por |
oaire.citationVolume | 5140 | por |
dc.identifier.doi | 10.1007/978-3-540-79980-1_7 | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Lecture Notes in Computer Science | por |
sdum.conferencePublication | ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS | por |
Aparece nas coleções: | HASLab - Artigos em revistas internacionais DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
AMAST08-BOS.pdf | preprint | 522,25 kB | Adobe PDF | Ver/Abrir |