[Caml-list] Oregon Programming Languages Summer School 2011 - Call For Participation

[Caml-list] Oregon Programming Languages Summer School 2011 - Call For Participation

[marco.gaboardi]

----------------------------------------------------------------------

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