Everyday life is subject to the quality of computer and system software. The more our society depends on computing systems for critical aspects of economy, defense, and government, the more software correctness and reliability becomes crucial. The focus of this summer school is to cover "a spectrum of types", ranging from the very dynamic (such as contracts in untyped languages) to the very static (such as dependent types).
Our goal is to provide a unique opportunity for participants to understand the current landscape in programming language research. We will present a range of material, from foundational work on semantics and type theory to advanced program verification techniques, to experience with applying the theory. Lectures will include discussions of basic theoretical tools such as proof theory, type theory, abstract interpretation and their connection to programming language semantics. The lectures will describe how these ideas can be applied to yield proved-correct software by introducing students and researchers to the ideas of software verification and compiler correctness.
At all times, material will be presented at a tutorial level that will help graduate students and researchers understand the critical issues and open problems confronting the field. We hope that students will be able to apply what they learn at the school in their own research. We believe that by doing so the school will have a broad impact on the next generation of software, programming language and software engineering researchers in industry and academia.
The conference is open to anyone interested. Prerequisites are knowledge of programming languages at the level provided by an undergraduate survey course. Our primary target group is first- or second-year graduate students. We also expect attendance by post-doc researchers and faculty members who would like to conduct research on this topic or introduce new courses at their universities. For the first time, we have added three days of reviews for those students who would benefit from a deeper understanding of basic concepts.