“Types, Logic, Semantics, & Verification”
June 15-17

REGISTRATION DEADLINE: MARCH 16, 2015

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.

The goal of this program 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. The hope is that students will be able to apply what they learn at the school in their own research. They 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. The primary target group is first- or second-year graduate students. Post-doc researchers and faculty members who would like to conduct research on this topic or introduce new courses at their universities are also welcome.

For more details on registration, scheduling, organizers, and speakers for the summer school, please visit the Oregon Programming Languages Summer School website here.