University of Oregon — Department of Computer and Information Science

Oregon Programming Language Summer School

Types, Logic, Semantics, and Verification

Eugene OR

June 15-29, 2014


Oregon Programming Languages Summer School — June 16-28, 2014

Types, Logic, Semantics, and Verification

All sessions will be held in Room 110 of the Knight Law Center on the University of Oregon campus.

Coq Boot Camp

For students who wish to brush up on their skills using the Coq Proof Assistant, the Boot Camp will be run by Michael Clarkson on Sunday, 6/15. It starts at 9AM and lasts until 5PM with a 2-hour break from Noon to 2PM.

Lecture Schedule

The program consists of a series of 40 lectures and 11 hands-on sessions. The sessions are non-overlapping, so participants will have the opportunity to attend all lectures. Each lecture is 80 minutes, including time for questions.

Morning Afternoon Evening
Date Session 1 Session 2 Session 1 Session 2
MON 6/16 Zdancewic Weirich Zdancewic Hands-On Session
TUE 6/17 Weirich Zdancewic Birkedal Hands-On Session Student Talks
WED 6/18 Zdancewic Pientka Weirich Hands-On Session
THR 6/19 Birkedal Pientka Weirich Hands-On Session Student Talks
FRI 6/20 Birkedal Pientka Birkedal Hands-On Session
SAT 6/21 Pientka Birkedal Harper Hands-On Session
SUN 6/22 Excursion
MON 6/23 Appel Harper Appel Hands-On Session
TUE 6/24 Appel Norell Harper Hands-On Session Student Talks
WED 6/25 Norell Morrisett Dreyer Harper Student Talks
THR 6/26 Appel Dreyer Morrisett Ball
FRI 6/27 Morrisett Norell Dreyer Hands-On Session
SAT 6/28 Dreyer Norell Morrisett Hands-On Session

Lectures are held in 110 Knight Law Center. Morning sessions begin at 9:00 AM and run until noon. Afternoon sessions begin at 2:00 PM and run until 5:00 PM. Evening Lectures are at 7:00 PM.

Student Talks

Student talks are held to give the students the opportunity to share their areas of research. Most talks deal with as yet unpublished and unfinished research. Student talks are held in 220 Deschutes Hall.

Date Time Speaker Topic
TUE 6/17 8:00 PM Pavel Panchekha Improving numerical precision of floating-point programs
8:30 PM Chad Nester Turing Categories
9:00 PM Phil Nguyễn Soft Contract Verification
9:30 PM Wilayat Khan Web session security guarantees using Coq
THR 6/19 8:00 PM Jesper Cockx Pattern matching in homotopy type theory
8:30 PM Steve Huntsman An application of category theory to nonlinear dimensionality reduction
9:00 PM Laure Thompson
Matthew Milano
Deciding Program Equivalence Efficiently for Software-Defined Networks: A Coalgebraic Decision Procedure for NetKAT
9:45 PM Mario Alvarez Using computational reflection to improve proof automation in the Verified Software Toolchain
TUE 6/24 7:00 PM Hannah Gommerstadt Fighting Cryptographic Misuse with Types
7:30 PM Greg Sullivan The role of verification in the design of a clean-slate architecture, programming languages, and OS -- the SAFE project.
8:00 PM Doug Woos Verified Distributed Systems
8:30 PM Ahmad Salim Al-Sibahi Scrapping Your Dependently-Typed Boilerplate is Hard
9:00 PM Rodolphe Lepigre An introduction to (Classical) Realizability
WED 6/25 8:00 PM Konstantin Weitz BGP (Border Gateway Protocol) misconfigurations cause severe problems on the internet, e.g. the takedown of YouTube. We generate and verify BGP configurations in Coq, proving properties such as correctness and profit maximization.
8:30 PM John Phelps UMX: The UTF8 Metalanguage eXtensions
9:00 PM Dan DaCosta We will present a formalization of a simple imperative programming language's evaluation semantics in Lolli, a fragment of linear logic. Lolli admits uniform provability giving rise to a syntax-directed proof procedure. There *seems* to be a close relationship between derivations in the object system and uniform proofs in the object system's formalization. This *may* make informal intuitions more pertinent to formalizations.
9:20 PM Sandro Stucki Graph rewriting for biochemical modeling
Copyright © University of Oregon Department of Computer and Information Science. All rights reserved.
Privacy Policy