[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
----------------------------------------------------------------------
Call For Participation
Types, Semantics and Verification
10th Annual Oregon Programming Languages Summer School (OPLSS 2011)
University of Oregon, Eugene. June 16 - July 1, 2011
http://www.cs.uoregon.edu/Activities/summerschool/
=> NOTE: the registration deadline has passed but we still have few
open slots.
----------------------------------------------------------------------
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 Oregon Programming Languages Summer School (OPLSS) has been held
at the University of Oregon each summer since 2002. This year, in the
occasion of the tenth anniversary of the summer school, two plenary
lectures will complement the technical program.
----------------------------------------------------------------------
Technical Program
Logical Relations
Amal Ahmed - Indiana University
Software Verification
Andrew Appel - Princeton University
Monadic Effects
Nick Benton - Microsoft Research
Metamathematics of Polymorphic Logics - applications
Robert Constable - Cornell University
Polarization and Focalization
Pierre-Louis Curien - pi.r2 team, PPS, CNRS-Paris Diderot University-
INRIA
Type Theory Foundation
Robert Harper - Carnegie Mellon University
The Calculus of Inductive Constructions
Hugo Herbelin - pi.r2 team, PPS, CNRS-Paris Diderot University-INRIA
Compiler Certification
Xavier Leroy - INRIA
Programming languages in string diagrams
Paul-Andre' Mellies - PPS, CNRS-Paris Diderot University
Imperative Programming in Coq
Greg Morrisett - Harvard University
Proof Theory Foundation
Frank Pfenning - Carnegie Mellon University
Proof Theory in Coq
Benjamin Pierce - University of Pennsylvania
Semilattices, Domains, and Computability
Dana Scott - Carnegie Mellon University - Berkeley University
----------------------------------------------------------------------
Plenary Lectures:
Speaker: Dana Scott (Carnegie Mellon University and Berkeley University)
Title: What is a Proof? -- Some Challenges for Automated Theorem Proving
Speaker: Robert Constable (Cornell University)
Title: Metamathematics of Polymorphic Logics - foundations
----------------------------------------------------------------------
Registration
=> the registration deadline has passed but we still have few open
slots.
Full information on registration are available at:
http://www.cs.uoregon.edu/Activities/summerschool/
----------------------------------------------------------------------
Some further activities will complement the main program.
Coq-labs:
Some of the lectures will assume interactive sessions using the
interactive proof assistant Coq. Students are encouraged to bring a
laptop on which Coq has been installed, and to form small working
group during the interactive sessions. Moreover, some Coq-labs will be
offered in order to give the participants the opportunity of make more
practice in using Coq.
Student Sessions:
Interested students will have the opportunity to present their work
during special sessions. Each presentation will consist of a brief
talk about the student research interests and results. These sessions
will be an occasion for students to obtain useful feedback on their
work by other students and researchers, and also to interact with
participants having similar research interests.
We hope to see you in Eugene.
Zena Ariola
Pierre-Louis Curien
Marco Gaboardi
Robert Harper
Hugo Herbelin
