An important consequence of only having value types in an aliasing-free programming language is the significant reduction in annotation burden to verify programs using semi-automatic proof systems. However, values in such language are often copied implicitly which is detrimental to the execution speed and memory usage of practical systems. Moreover, embedded systems programmers need fine-grained control over the circumstances at which data is copied to be able to predict memory use and execution times.