Preliminary Announcement Summer School on the Proofs-as-Programs Paradigm Eugene, Oregon, USA June 24 - July 5, 2002 Supported by NSF, ACM SIGPLAN, the University of Oregon, Indiana University, Oregon Graduate Institute, and INRIA. Organizers: Zena Ariola (University of Oregon) Hugo Herbelin (INRIA) Amr Sabry (Indiana University) Scientific committee: Thierry Coquand (Chalmers University) Pierre-Louis Curien (University of Paris 7) Robert Harper (Carnegie Mellon University) Frank Pfenning (Carnegie Mellon University) Benjamin Pierce (University of Pennsylvania) Carsten Schuermann (Yale University) Objective: The summer school on the "Proofs-as-Programs Paradigm" is a two week course for computer scientists and mathematicians interested in formal systems and automated techniques for reasoning about programs, with particular emphasis on the use of types as specifications for modern software components. The school is especially suitable for graduate students who need to extend their background in mathematics, logic, and type theory, and wish to gain experience working with logical frameworks and proof assistants. The curriculum includes basic foundational material for all attendees, advanced material for those interested in new research directions, and experience in using various tools for those interested in practical applications. School attendance is open to anyone meeting the prerequisites, subject to the availability of space. Prerequisites are undergraduate knowledge of logic, mathematics, and programming languages. Graduate students who wish to attend should send an application consisting of a short description of their educational background and one letter of reference. We anticipate making available a number of grants to cover travel and lodging costs for qualified graduate students. The school will be held on the University of Oregon campus in Eugene, Oregon. Eugene is a lively place with access to exquisite nature: ocean beaches, forests, mountains, and desert all within a few hours drive. Concurrent with the school, the Oregon Bach festival will be presenting nightly concerts that showcase a variety of musical styles. A web site with more information about the content of the summer school and how to submit the applications will be available soon. In the meantime you can direct your questions to proofsasprograms@cs.uoregon.edu. ---------------------------------------------------------------------- Preliminary program Basic topics: - Logical Structures ( lecturer to be announced) - Type Systems (Herman Geuvers - Nijmegen University - to be confirmed) - Inductive Types ( lecturer to be announced) - Linear Logic (Harry Mairson - Brandeis University - to be confirmed ) - Decidability of Type Checking (Dale Miller - Pennsylvania State University) Advanced topics: - Computational Content of Classical Logic (Hugo Herbelin - INRIA) - Realizability and Program Extraction (Stefano Berardi - Universita' di Torino) - Computation and Normalization as Interaction (Pierre-Louis Curien - University of Paris 7 & CNRS) - Advanced Topics in Type Theory (Alexandre Miquel - Chalmers University, Sweden) Applications: - Hard-wired algorithms certification (Intel) - Formalization of mathematics - Protocols verification - Formal semantics of programming languages 16-Mar-2002 18:39:02 -0400,1103;000000000000-00000000