Abstract
We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a somewhat surprising static checking algorithm that makes use of a network flow property equivalent to the semantic condition via reduction to a satisfaction problem for a system of linear inequalities.
| Original language | English |
|---|---|
| Article number | 15 |
| Journal | ACM Transactions on Programming Languages and Systems |
| Volume | 30 |
| Issue number | 3 |
| DOIs | |
| Publication status | Published - 2008 May 1 |
| Externally published | Yes |
Fingerprint
Keywords
- Mutable state
- Side effects
ASJC Scopus subject areas
- Software
Cite this
Witnessing side effects. / Terauchi, Tachio; Aiken, Alex.
In: ACM Transactions on Programming Languages and Systems, Vol. 30, No. 3, 15, 01.05.2008.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - Witnessing side effects
AU - Terauchi, Tachio
AU - Aiken, Alex
PY - 2008/5/1
Y1 - 2008/5/1
N2 - We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a somewhat surprising static checking algorithm that makes use of a network flow property equivalent to the semantic condition via reduction to a satisfaction problem for a system of linear inequalities.
AB - We present a new approach to the old problem of adding global mutable state to purely functional languages. Our idea is to extend the language with "witnesses," which is based on an arguably more pragmatic motivation than past approaches. We give a semantic condition for correctness and prove it is sufficient. We also give a somewhat surprising static checking algorithm that makes use of a network flow property equivalent to the semantic condition via reduction to a satisfaction problem for a system of linear inequalities.
KW - Mutable state
KW - Side effects
UR - http://www.scopus.com/inward/record.url?scp=44249094188&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=44249094188&partnerID=8YFLogxK
U2 - 10.1145/1353445.1353449
DO - 10.1145/1353445.1353449
M3 - Article
VL - 30
JO - ACM Transactions on Programming Languages and Systems
JF - ACM Transactions on Programming Languages and Systems
SN - 0164-0925
IS - 3
M1 - 15
ER -