SHF: Small: SEQUBE: A Sequent Calculus Foundation for High- Level and Intermediate Programming Languages

点击翻译按钮获取中文摘要

Title: SHF:Small:SEQUBE:A Sequent Calculus Foundation for High-Level and Intermediate Programming LanguagesModern programming languages are complex. They provide sophisticated control mechanisms, offer a combination of different programming paradigms (e.g., functional or object-oriented), and allow the definition of infinite objects and processes (e.g., servers or operating systems). To have assurance in our software, it is fundamentally important to have a simple and intuitive framework for reasoning about and experimenting with programs that use these features: both for programming language designers and implementors, as well as for programmers who need to prove safety properties of critical applications.Traditionally, the lambda-calculus has served as a foundation for writing and proving properties of programs. The intellectual merit of this research consists of developing an alternative model of programs based on the sequent calculus. Instead of starting from a core language and layering features on top as needed, the new model naturally includes these features from the beginning. Like the lambda-calculus, the sequent-based model originates from logic, but is rooted in the concept of duality that provides two ways to approach problems, where one is often more familiar. Additionally, the sequent-based model provides a new way to organize intermediate languages used in compilers to aid program optimization and analysis.The broader impact of the research consists of providing a vehicle for disseminating knowledge between different communities. Since the new model includes both the functional and object-oriented paradigms naturally as duals, it provides a logical interpretation of languages, such as Scala, that merge the two approaches. In addition, the research will explore ways to incorporate reasoning about infinite processes and computational effects in a proof assistant. Lastly, an emphasis on duality is beneficial for education; given two possible explanations, students can be introduced to the more familiar one first when introducing difficult ideas, while using existing knowledge and intuition to explore new concepts.