SHF: Small: A Foundation for Effects

现代编程语言提供了复杂的控制机制，使它们适合对各种应用程序进行编程。如何在不造成不一致的情况下将这些功能组合在一起，或者让程序员了解如何使用它们，这对语言设计人员来说是一项挑战。该工作旨在提供一个健全和健壮的框架，以孤立地推理各种控制机制，更重要的是它们之间的复杂相互作用。Curry-Howard同构将指导这样一个框架的发展，这需要将编程语言与逻辑联系起来。与逻辑的联系允许人们形式化关于表达能力的问题，并与证明理论领域交换和借用结果。将研究直接表达动态属性的新逻辑，而不是通过程序转换。这种方法的一个优点是编译、执行、优化和代码安全都是在同一基础级别上表达的，这项研究将直接影响如何推理安全属性，因为它提供了在不断变化的上下文中推理动态属性的方法。它还将对程序验证产生影响，因为它提供了对程序应该满足的不变量的更好的理解。

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.