Vasudeo, Jyotindra2014-03-142014-03-142006-05-05etd-05252006-171343http://hdl.handle.net/10919/33228Aliasing complicates both formal and informal reasoning and is a particular problem in object-oriented languages, where variables denote references to objects rather than object values. Researchers have proposed various approaches to the aliasing problem in object-oriented languages, but all use reference semantics to reason about programs. This thesis describes the design and implementation of Tako—a Java-like language that facilitates value semantics by incorporating alias-avoidance. The thesis describes a non-trivial application developed in the Tako language and discusses some of the object-oriented programming paradigm shifts involved in translating that application from Java to Tako. It introduces a proof rule for procedure calls that uses value semantics and accounts for both repeated arguments and subtyping.In CopyrightLanguage DesignAliasingTakoJavaFormal ReasoningCompilersThesishttp://scholar.lib.vt.edu/theses/available/etd-05252006-171343/