File Download
There are no files associated with this item.
Links for fulltext
(May Require Subscription)
- Publisher Website: 10.1017/S0956796812000354
- Scopus: eid_2-s2.0-84867536767
- WOS: WOS:000309725700003
- Find via
Supplementary
- Citations:
- Appears in Collections:
Article: MRI: Modular reasoning about interference in incremental programming
Title | MRI: Modular reasoning about interference in incremental programming |
---|---|
Authors | |
Issue Date | 2012 |
Publisher | Cambridge 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? |
Abstract | Incremental 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 Identifier | http://hdl.handle.net/10722/188521 |
ISSN | 2023 Impact Factor: 1.1 2023 SCImago Journal Rankings: 0.484 |
ISI Accession Number ID | |
References |
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Oliveira, BCDS | en_US |
dc.contributor.author | Schrijvers, T | en_US |
dc.contributor.author | Cook, WR | en_US |
dc.date.accessioned | 2013-09-03T04:09:42Z | - |
dc.date.available | 2013-09-03T04:09:42Z | - |
dc.date.issued | 2012 | en_US |
dc.identifier.citation | Journal Of Functional Programming, 2012, v. 22 n. 6, p. 797-852 | en_US |
dc.identifier.issn | 0956-7968 | en_US |
dc.identifier.uri | http://hdl.handle.net/10722/188521 | - |
dc.description.abstract | Incremental 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.language | eng | en_US |
dc.publisher | Cambridge University Press. The Journal's web site is located at http://journals.cambridge.org/action/displayJournal?jid=JFP | en_US |
dc.relation.ispartof | Journal of Functional Programming | en_US |
dc.title | MRI: Modular reasoning about interference in incremental programming | en_US |
dc.type | Article | en_US |
dc.identifier.email | Oliveira, BCDS: oliveira@comp.nus.edu.sg | en_US |
dc.identifier.authority | Oliveira, BCDS=rp01786 | en_US |
dc.description.nature | link_to_subscribed_fulltext | en_US |
dc.identifier.doi | 10.1017/S0956796812000354 | en_US |
dc.identifier.scopus | eid_2-s2.0-84867536767 | en_US |
dc.relation.references | http://www.scopus.com/mlt/select.url?eid=2-s2.0-84867536767&selection=ref&src=s&origin=recordpage | en_US |
dc.identifier.volume | 22 | en_US |
dc.identifier.issue | 6 | en_US |
dc.identifier.spage | 797 | en_US |
dc.identifier.epage | 852 | en_US |
dc.identifier.isi | WOS:000309725700003 | - |
dc.publisher.place | United Kingdom | en_US |
dc.identifier.scopusauthorid | Oliveira, BCDS=12239474400 | en_US |
dc.identifier.scopusauthorid | Schrijvers, T=8870481000 | en_US |
dc.identifier.scopusauthorid | Cook, WR=11939670900 | en_US |
dc.identifier.issnl | 0956-7968 | - |