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 implementation.
Australasian Computer Science Week Multiconference, Geelong, Australia 31 January - 3 February 2017
Proceedings of the Australasian Computer Science Week Multiconference /