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 the mix or interplay of theory and practice in program verification. The main aim is to enable participants to conduct research in the area, thereby contributing to improve software quality.
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, category theory 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. The lectures will also introduce the participants to the use of the proof assistant Coq in order to provide machine-checked proofs of program 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 course 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.