- BS, 1980, University of Pisa, Italy
- PhD, 1992, Harvard University
Dr. Zena M. Ariola is a Professor in the Department of Computer and Information Science at the University of Oregon. Ariola received the Laurea degree summa cum laude in Informatics from the University of Pisa in 1980. She received the Ph.D. degree in Computer Science from Harvard University in 1992.
From 1981 to 1986, Ariola worked at the Olivetti corporation in Pisa, Italy. She also worked as a consultant on the Ada language for the SPL Corporation in Abingdon, United Kindom, and for the General System Group (GSG) in Salem, NH. In 1992, Ariola joined the faculty at Oregon. She also had visiting positions at the Centre for Mathematics and Computer Science (CWI) and Vrije Universiteit in Amsterdam, The Netherlands. Dr. Ariola was awarded the NSF Research Initiation Award in 1994 and the NSF Career award in 1996. She was promoted to Full Professor in 2006.
Dr. Ariola's research interests are in the foundation of programming languages and in high-level hardware description languages.
In 1968 Dijkstra, in his seminal paper "Go To Statement Considered Harmful", proposed that goto statements should be abolished from all high-level programming languages. However, with the advent of the worldwide web, operators that allow one to modify the control flow of a program are not only useful but are necessary to model daily computer interactions. This raises the need to understand control flow operators, their semantics and their expressive power. Dr. Ariola follows the Curry-Howard approach in establishing a connection between these operators and mathematical proof principles. Connections with logics developed in the linguistic setting are also investigated with the aim to introduce a novel framework to reason about dynamic features. The applicability of the developed techniques to security is also considered.
High-level languages are also employed in the context of hardware design in both microprocessor architectures and mobile phones. These are not general-purpose languages; they describe finite state transition systems and are commonly based on Guarded Atomic Actions. A hardware component is described by a module. To achieve better physical requirements, it is not uncommon for designers to make changes which translate into a module refinement. Dr. Ariola's research focuses on developing useful frameworks for reasoning about correctness of the refinement.