ACL --- Eliminating Parameter Aliasing with Dynamic Dispatch by Gary T. Leavens and Olga Antropova Abstract We have designed and prototyped a new approach for eliminating reference parameter aliases. This approach allows procedure calls with overlapping call-by-reference parameters, but guarantees that procedure bodies are alias-free. It involves writing multiple bodies for a procedure: up to one body for each possible aliasing combination. Procedure calls are dispatched to the appropriate procedure body based on the alias combination that occurs among the actual parameters and imported global variables; errors are generated if there is no corresponding body. This approach makes writing verifiable client code simpler, since clients do not need to write code to determine the aliasing combination among actuals. Furthermore, since procedure bodies are free of aliases, their static analysis and verification is easier. The prototype language we have designed to explore these ideas incorporates some features to limit the number of alternative procedure bodies that a programmer must write. Keywords: reference parameter aliasing, global variable aliasing, multibody procedures, dynamic dispatch, static dispatch, program verification, ACL language, static analysis, call-by-reference. 1997 CR Categories: D.3.1 [Programming Languages] Formal Definitions and Theory --- semantics; D.3.3 [Programming Languages] Language Constructs and Features --- control structures, procedures, functions, and subroutines; D.3.m [Programming Languages] Miscellaneous --- dynamic dispatch, multiple dispatch; F.3.1 [Logics and Meanings of Programs] Specifying and Verifying and Reasoning about Programs --- logics of programs.