Special Projects: Proofs as Programs

University Of Oregon Eugene, Eugene OR

Investigators

Abstract

EIA-0214927 Ariola, Zena University of Oregon Special Projects: Proofs as Programs The University of Oregon at Eugene has been provided with support to organize a summer school on the increasingly important paradigm of proofs-as-programs. According to this paradigm a typing assertion M: A has several "isomorphic" interpretations. In the computational interpretation, M is a (functional) program and the type A is its specification. In the logical interpretation M is a proof of the proposition A. The discovery of the connection between the two interpretations is due to Curry, Howard, and DeBruijn. Fifty years later, this connection between proofs and programs is now established as the foundation of many formal systems and automated techniques for reasoning about programs. The aim of the school is to prepare interested graduate students, academics, and software engineers for conducting research in the area. The curriculum will include basic foundational material for all attendees; advanced material for those interested in new research directions; and a review of various tools together with experience in using them for various tasks for those interested in practical applications. In more detail, the curriculum will include the following three major categories of lectures: 1. Background: This material consists of well-established results developed in the late 80's and early 90's. This background information will provide an introduction to the essential concepts and methodologies of the paradigm. 2. Advanced Topics: This material consists of more recent results that extend and generalize the earlier work. This will provide students with insights into research and open questions. 3. Applications: This material will demonstrate how theoretical results can be used by practitioners in various fields of computer science. This will provide students with skills in the use of formal methods to reason about and generate solutions to practical problems, such as verification of hardware protocols and Java specifications.