Static techniques for reducing memory usage in the C implementation of whiley programs

Languages that use call-by-value semantics, such as Whiley, can make program verification easier. But efficient implementation becomes harder, due to the overhead of copying and garbage collection. This paper describes how a mixture of static analysis and runtime-monitoring can be used to eliminate unnecessary copying and deallocate memory without garbage collection. We show that this allows Whiley programs to be translated into efficient C implementations.