Title: MRI: Modular reasoning about interference in incremental programming
Authors: Oliveira, Bruno C. D. S ×
Schrijvers, Tom
Cook, William R #
Issue Date: 2012
Publisher: Cambridge University Press
Series Title: Journal of Functional Programming vol:22 pages: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.
ISSN: 0956-7968
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Non-KU Leuven Association publications
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
jfp_mri.pdfarticle Published 340KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science