File Download

There are no files associated with this item.

  Links for fulltext
     (May Require Subscription)
Supplementary

Article: MRI: Modular reasoning about interference in incremental programming

TitleMRI: Modular reasoning about interference in incremental programming
Authors
Issue Date2012
PublisherCambridge University Press. The Journal's web site is located at http://journals.cambridge.org/action/displayJournal?jid=JFP
Citation
Journal Of Functional Programming, 2012, v. 22 n. 6, p. 797-852 How to Cite?
AbstractIncremental Programming (IP) is a programming style in which new program components are defined as increments of other components. Examples of IP mechanisms include Object-oriented programming inheritance, aspect-oriented programming advice, and feature-oriented programming. A characteristic of IP mechanisms is that, while individual components can be independently defined, the composition of components makes those components become tightly coupled, sharing both control and data flows. This makes reasoning about IP mechanisms a notoriously hard problem: modular reasoning about a component becomes very difficult; and it is very hard to tell if two tightly coupled components interfere with each other's control and data flows. This paper presents modular reasoning about interference (MRI), a purely functional model of IP embedded in Haskell. MRI models inheritance with mixins and side effects with monads. It comes with a range of powerful reasoning techniques: equational reasoning, parametricity, and reasoning with algebraic laws about effectful operations. These techniques enable MRI in the presence of side effects. MRI formally captures harmlessness, a hard-to-formalize notion in the interference literature, in two theorems. We prove these theorems with a non-trivial combination of all three reasoning techniques. ©2012 Copyright Cambridge University Press.
Persistent Identifierhttp://hdl.handle.net/10722/188521
ISSN
2015 Impact Factor: 1.357
2015 SCImago Journal Rankings: 0.917
ISI Accession Number ID
References

 

DC FieldValueLanguage
dc.contributor.authorOliveira, BCDSen_US
dc.contributor.authorSchrijvers, Ten_US
dc.contributor.authorCook, WRen_US
dc.date.accessioned2013-09-03T04:09:42Z-
dc.date.available2013-09-03T04:09:42Z-
dc.date.issued2012en_US
dc.identifier.citationJournal Of Functional Programming, 2012, v. 22 n. 6, p. 797-852en_US
dc.identifier.issn0956-7968en_US
dc.identifier.urihttp://hdl.handle.net/10722/188521-
dc.description.abstractIncremental Programming (IP) is a programming style in which new program components are defined as increments of other components. Examples of IP mechanisms include Object-oriented programming inheritance, aspect-oriented programming advice, and feature-oriented programming. A characteristic of IP mechanisms is that, while individual components can be independently defined, the composition of components makes those components become tightly coupled, sharing both control and data flows. This makes reasoning about IP mechanisms a notoriously hard problem: modular reasoning about a component becomes very difficult; and it is very hard to tell if two tightly coupled components interfere with each other's control and data flows. This paper presents modular reasoning about interference (MRI), a purely functional model of IP embedded in Haskell. MRI models inheritance with mixins and side effects with monads. It comes with a range of powerful reasoning techniques: equational reasoning, parametricity, and reasoning with algebraic laws about effectful operations. These techniques enable MRI in the presence of side effects. MRI formally captures harmlessness, a hard-to-formalize notion in the interference literature, in two theorems. We prove these theorems with a non-trivial combination of all three reasoning techniques. ©2012 Copyright Cambridge University Press.en_US
dc.languageengen_US
dc.publisherCambridge University Press. The Journal's web site is located at http://journals.cambridge.org/action/displayJournal?jid=JFPen_US
dc.relation.ispartofJournal of Functional Programmingen_US
dc.titleMRI: Modular reasoning about interference in incremental programmingen_US
dc.typeArticleen_US
dc.identifier.emailOliveira, BCDS: oliveira@comp.nus.edu.sgen_US
dc.identifier.authorityOliveira, BCDS=rp01786en_US
dc.description.naturelink_to_subscribed_fulltexten_US
dc.identifier.doi10.1017/S0956796812000354en_US
dc.identifier.scopuseid_2-s2.0-84867536767en_US
dc.relation.referenceshttp://www.scopus.com/mlt/select.url?eid=2-s2.0-84867536767&selection=ref&src=s&origin=recordpageen_US
dc.identifier.volume22en_US
dc.identifier.issue6en_US
dc.identifier.spage797en_US
dc.identifier.epage852en_US
dc.identifier.isiWOS:000309725700003-
dc.publisher.placeUnited Kingdomen_US
dc.identifier.scopusauthoridOliveira, BCDS=12239474400en_US
dc.identifier.scopusauthoridSchrijvers, T=8870481000en_US
dc.identifier.scopusauthoridCook, WR=11939670900en_US

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats