[Agda] 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