A Step-Indexed Kripke Model of Hidden State

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 350
  • Download : 0
DC FieldValueLanguage
dc.contributor.authorSchwinghammer, Janko
dc.contributor.authorBirkedal, Larsko
dc.contributor.authorPottier, Francoisko
dc.contributor.authorReus, Bernhardko
dc.contributor.authorStovring, Kristianko
dc.contributor.authorYang, Hongseokko
dc.date.accessioned2017-08-08T06:54:16Z-
dc.date.available2017-08-08T06:54:16Z-
dc.date.created2017-08-02-
dc.date.created2017-08-02-
dc.date.created2017-08-02-
dc.date.created2017-08-02-
dc.date.issued2013-02-
dc.identifier.citationMATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, v.23, no.1, pp.1 - 54-
dc.identifier.issn0960-1295-
dc.identifier.urihttp://hdl.handle.net/10203/225275-
dc.description.abstractFrame and anti-frame rules have been proposed as proof rules for modular reasoning about programs. Frame rules allow the hiding of irrelevant parts of the state during verification, whereas the anti-frame rule allows the hiding of local state from the context. We discuss the semantic foundations of frame and anti-frame rules, and present the first sound model for Chargueraud and Pottier's type and capability system including both of these rules. The model is a possible worlds model based on the operational semantics and step-indexed heap relations, and the worlds are given by a recursively defined metric space. We also extend the model to account for Pottier's generalised frame and anti-frame rules, where invariants are generalised to families of invariants indexed over preorders. This generalisation enables reasoning about some well-bracketed as well as (locally) monotone uses of local state.-
dc.languageEnglish-
dc.publisherCAMBRIDGE UNIV PRESS-
dc.titleA Step-Indexed Kripke Model of Hidden State-
dc.typeArticle-
dc.identifier.wosid000312392100001-
dc.identifier.scopusid2-s2.0-84871341121-
dc.type.rimsART-
dc.citation.volume23-
dc.citation.issue1-
dc.citation.beginningpage1-
dc.citation.endingpage54-
dc.citation.publicationnameMATHEMATICAL STRUCTURES IN COMPUTER SCIENCE-
dc.identifier.doi10.1017/S0960129512000035-
dc.contributor.localauthorYang, Hongseok-
dc.contributor.nonIdAuthorSchwinghammer, Jan-
dc.contributor.nonIdAuthorBirkedal, Lars-
dc.contributor.nonIdAuthorPottier, Francois-
dc.contributor.nonIdAuthorReus, Bernhard-
dc.contributor.nonIdAuthorStovring, Kristian-
dc.description.isOpenAccessN-
dc.type.journalArticleArticle-
dc.subject.keywordPlusHIGHER-ORDER STORE-
dc.subject.keywordPlusSEPARATION LOGIC-
dc.subject.keywordPlusRECURSIVE TYPES-
dc.subject.keywordPlusSEMANTICS-
dc.subject.keywordPlusABSTRACTION-
dc.subject.keywordPlusRESOURCES-
dc.subject.keywordPlusWORLDS-
Appears in Collection
CS-Journal Papers(저널논문)
Files in This Item
There are no files associated with this item.

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0