Ghent University Academic Bibliography

Advanced

MRI: modular reasoning about interference in incremental programming

Bruno CdS Oliveira, Tom Schrijvers UGent and William Cook (2012) JOURNAL OF FUNCTIONAL PROGRAMMING. 22(6). p.797-852
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 (OOP) inheritance, aspect-oriented programming (AOP) advice and feature-oriented programming (FOP). 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 modular reasoning about interference 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.
Please use this url to cite or link to this publication:
author
organization
year
type
journalArticle (original)
publication status
published
subject
keyword
modular reasoning, parametricity, functional programming, interference, Haskell, side effects, monads, algebraic laws, equational reasoning, inheritance, modularity, programming languages, mixins, aspect-oriented programming
journal title
JOURNAL OF FUNCTIONAL PROGRAMMING
J. Funct. Program
volume
22
issue
6
pages
797 - 852
Web of Science type
Article
Web of Science id
000309725700003
JCR category
COMPUTER SCIENCE, SOFTWARE ENGINEERING
JCR impact factor
0.943 (2012)
JCR rank
58/104 (2012)
JCR quartile
3 (2012)
ISSN
0956-7968
DOI
10.1017/S0956796812000354
language
English
UGent publication?
yes
classification
A1
copyright statement
I have transferred the copyright for this publication to the publisher
id
2972921
handle
http://hdl.handle.net/1854/LU-2972921
date created
2012-08-20 10:18:20
date last changed
2013-07-15 11:43:06
@article{2972921,
  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 (OOP) inheritance, aspect-oriented programming (AOP) advice and feature-oriented programming (FOP).  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 modular reasoning about interference 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.},
  author       = {Oliveira, Bruno CdS and Schrijvers, Tom and Cook, William},
  issn         = {0956-7968},
  journal      = {JOURNAL OF FUNCTIONAL PROGRAMMING},
  keyword      = {modular reasoning,parametricity,functional programming,interference,Haskell,side effects,monads,algebraic laws,equational reasoning,inheritance,modularity,programming languages,mixins,aspect-oriented programming},
  language     = {eng},
  number       = {6},
  pages        = {797--852},
  title        = {MRI: modular reasoning about interference in incremental programming},
  url          = {http://dx.doi.org/10.1017/S0956796812000354},
  volume       = {22},
  year         = {2012},
}

Chicago
Oliveira, Bruno CdS, Tom Schrijvers, and William Cook. 2012. “MRI: Modular Reasoning About Interference in Incremental Programming.” Journal of Functional Programming 22 (6): 797–852.
APA
Oliveira, B. C., Schrijvers, T., & Cook, W. (2012). MRI: modular reasoning about interference in incremental programming. JOURNAL OF FUNCTIONAL PROGRAMMING, 22(6), 797–852.
Vancouver
1.
Oliveira BC, Schrijvers T, Cook W. MRI: modular reasoning about interference in incremental programming. JOURNAL OF FUNCTIONAL PROGRAMMING. 2012;22(6):797–852.
MLA
Oliveira, Bruno CdS, Tom Schrijvers, and William Cook. “MRI: Modular Reasoning About Interference in Incremental Programming.” JOURNAL OF FUNCTIONAL PROGRAMMING 22.6 (2012): 797–852. Print.