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.