---------------------------------------------------------------------- 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/ => Registration Deadline: March 4, 2011 ---------------------------------------------------------------------- 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 Full information on registration are available at: http://www.cs.uoregon.edu/Activities/summerschool/ Registration Deadline: March 4, 2011 ---------------------------------------------------------------------- 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