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 |