Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Oregon Programming Languages Summer School 201...


view this post on Zulip Email Gateway (Aug 18 2022 at 17:23):

From: Marco Gaboardi <gaboardi@cs.unibo.it>


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


Last updated: May 06 2024 at 12:29 UTC