[Prev][Next][Index][Thread]
Summer School on the Proofs-as-Programs Paradigm
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