From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6556 Path: news.gmane.org!not-for-mail From: Marco Gaboardi Newsgroups: gmane.comp.science.types.announce,gmane.science.mathematics.categories Subject: Oregon Programming Languages Summer School 2011 - Second Call For Participation Date: Tue, 1 Mar 2011 23:34:12 +0100 Message-ID: <4F364806-BB80-43F0-960A-977A688B2552@cs.unibo.it> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v936) Content-Type: text/plain; charset="us-ascii"; Format="flowed"; DelSp="yes" Content-Transfer-Encoding: 7bit X-Trace: dough.gmane.org 1299019320 32371 80.91.229.12 (1 Mar 2011 22:42:00 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Tue, 1 Mar 2011 22:42:00 +0000 (UTC) To: types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org, ProofTheory.List-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org, ic.eatcs-6l1t1zIuRx01GQ1Ptb7lUw@public.gmane.org, categories-59hdLBrVOVU@public.gmane.org Original-X-From: types-announce-bounces-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org Tue Mar 01 23:41:55 2011 Return-path: Envelope-to: gcst-types-announce-Uylq5CNFT+jYtjvyW6yDsg@public.gmane.org Original-Received: from rhizome.seas.upenn.edu ([158.130.69.24]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1PuYGO-0008Ms-Hm; Tue, 01 Mar 2011 23:41:52 +0100 Original-Received: from RHIZOME.SEAS.UPENN.EDU (LOCALHOST.upenn.edu [127.0.0.1]) by rhizome.seas.upenn.edu (8.14.3/8.14.3) with ESMTP id p21MdTFn024305; Tue, 1 Mar 2011 17:39:44 -0500 X-Mailman-Handler: $Id: mm-handler,v 1.2 2002/04/05 19:41:09 bwarsaw Exp $ Original-Received: from sympathy.seas.upenn.edu (sympathy.seas.upenn.edu [158.130.69.34]) by rhizome.seas.upenn.edu (8.14.3/8.14.3) with ESMTP id p21MYMIP024140 for ; Tue, 1 Mar 2011 17:34:22 -0500 Original-Received: from leb.cs.unibo.it (leb.cs.unibo.it [130.136.1.102]) by sympathy.seas.upenn.edu (8.14.3/8.13.6) with ESMTP id p21MYGq3022122 for ; Tue, 1 Mar 2011 17:34:22 -0500 Original-Received: from ssl.cs.unibo.it (ssl.cs.unibo.it [127.0.0.1]) (Authenticated sender: hidden) by leb.cs.unibo.it (Postfix) with ESMTPSA id 14F05355B5 ; Tue, 1 Mar 2011 23:34:13 +0100 (CET) X-Mailer: Apple Mail (2.936) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:5.2.15, 1.0.148, 0.0.0000 definitions=2011-03-01_05:2011-03-01, 2011-03-01, 1970-01-01 signatures=0 X-Spam-Level: X-Proofpoint-Spam-Details: rule=spam_score_tagging policy=default score=0 spamscore=0 ipscore=0 suspectscore=0 phishscore=0 bulkscore=21 adultscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=6.0.2-1012030000 definitions=main-1103010174 X-Proofpoint-SpamScore: 0 X-Mailman-Approved-At: Tue, 01 Mar 2011 17:39:27 -0500 X-BeenThere: types-announce-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org X-Mailman-Version: 2.1.12 Precedence: list List-Id: Announcements of interest to the TYPES community List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Original-Sender: types-announce-bounces-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org Errors-To: types-announce-bounces-nHFbR+4dATOoZA3Q9b/B0PZ8FUJU4vz8@public.gmane.org Xref: news.gmane.org gmane.comp.science.types.announce:2160 gmane.science.mathematics.categories:6556 Archived-At: [ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] ---------------------------------------------------------------------- Second 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