SHF: Small: A Foundation for Effects

University Of Oregon Eugene, Eugene OR

Investigators

Abstract

Modern programming languages provide sophisticated control mechanisms, making them suitable to program a wide variety of applications. It becomes a challenge for a language designer to bring together these features without creating inconsistencies or for a programmer to understand how to use them. The proposed work aims to provide a sound and robust framework for reasoning about a variety of control mechanisms in isolation and more importantly about the complex interactions among them. The Curry-Howard isomorphism will guide the development of such a framework, which entails connecting programming languages to logic. The connection to logic allows one to formalize questions regarding expressive power and to exchange and borrow results with the field of proof theory. New logics expressing dynamic properties directly, as opposed to through program transformations, will be investigated. An advantage of this approach is that compilation, execution, optimization and code safety are expressed within the same foundation level. The study will have a direct impact on how to reason about security properties, since it provides methods to reason about dynamic properties in a continuously changing context. It will also have an impact on program verification, since it provides a better understanding of the invariants that programs should satisfy.