Witnessing Side-Effects

Tachio Terauchi and Alexander Aiken

EECS Department, University of California, Berkeley

Technical Report No. UCB/CSD-05-1402

2005

This publication is archived. It is kept only for reference purposes, so it is no longer being updated and may not meet accessibility standards. If you need this content in a different format, please email webteam@eecs.berkeley.edu.

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2005/Archive/CSD-05-1402.pdf

We present a new approach to the old problem of adding side effects 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 static checking algorithm that makes use of a network flow property equivalent to the semantic condition.

BibTeX citation:

@techreport{Terauchi:CSD-05-1402,
    Author= {Terauchi, Tachio and Aiken, Alexander},
    Title= {Witnessing Side-Effects},
    Year= {2005},
    Month= {Jul},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2005/6471.html},
    Number= {UCB/CSD-05-1402},
    Abstract= {We present a new approach to the old problem of adding side effects 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 static checking algorithm that makes use of a network flow property equivalent to the semantic condition.},
}

EndNote citation:

%0 Report
%A Terauchi, Tachio 
%A Aiken, Alexander 
%T Witnessing Side-Effects
%I EECS Department, University of California, Berkeley
%D 2005
%@ UCB/CSD-05-1402
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2005/6471.html
%F Terauchi:CSD-05-1402