Oregon Programming Languages Summer School

Review

Prior to OPLSS, Paul Downen (University of Oregon) will conduct a review of type systems. This material can be found in Chapters 1-12, 23 and 24 from TAPL as well as Chapters 4-8, 10-11,16-17 from PFPL. This three-day session is separate from the OPLSS main program. The topics covered are:

Date	Topics
June 23	Lambda Calculus Products and Sums Operational semantics
June 24	Proof of Progress Proof of Preservation Recursive Types Polymorphism
June 25	Encodings Parametricity

Main Program

The program consists of thirty-seven 80-minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research. Most days, there is also a 80 minute hands-on session for participants to work through examples given in lecture.

Preparation

Prior to OPLSS, Video Participants should have this software installed on their laptops.

Useful references:

Chapter 1 of Type Driven Development in Idris (Chapter 1 is available free — see left side bar)
The Idris Tutorial

Schedule

Session 1	Session 2	Session 3	Session 4
Harper	Pfenning	Licata	Hands-On
Harper	Licata	Pfenning	Hands-On
Pfenning	Harper	Licata	Hands-On
Licata	Pfenning	Harper	Hands-On
Brady	Van Horn	Tobin-Hochstadt	Pfenning
Tobin-Hochstadt	Brady	Van Horn	Emacs Tutorial/Industry Experiences Board
Van Horn	Tobin-Hochstadt	Brady	Parametricity
Tobin-Hochstadt	Van Horn	Brady	Hands-On
Garcia	Ahmed	Krishnaswami	Hands-On
Ahmed	Krishnaswami	Garcia	Hands-On
Ahmed	Garcia	Krishnaswami	Hands-On
Garcia	Krishnaswami	Ahmed	Hands-On

Speaker	Affiliation	Topic
Amal Ahmed	Northeastern University	Correct and Secure Compilation for Multi-Language Software Relevent Papers Verified Compilers for a Multi-Language World (SNAPL'15) Linking Types for Multi-Language Software: Have Your Cake and Eat It Too Lecture Slides Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 \| Lecture 1, Video Part 5
Edwin Brady	University of St Andrews	Dependent Types in the Idris Programming Language Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 Lecture 2, Video Part 1 \| Lecture 2, Video Part 2 \| Lecture 2, Video Part 3 \| Lecture 2, Video Part 4 Lecture 3, Video Part 1 \| Lecture 3, Video Part 2 \| Lecture 3, Video Part 3 \| Lecture 3, Video Part 4 Lecture 4, Video Part 1 \| Lecture 4, Video Part 2 \| Lecture 4, Video Part 3 \| Lecture 4, Video Part 4
Ronald Garcia	University of British Colombia	Gradual Typing Lecture 1 Notes \| redex model for BA \| redex model for TBA Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 Lecture 2 Notes Lecture 2 Racket Exercise Partial Solution Lecture 3 Notes redex model for MBA
Robert Harper	Carnegie Mellon University	Programming Languages Background Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 Lecture 2, Video Part 1 \| Lecture 2, Video Part 2 \| Lecture 2, Video Part 3 \| Lecture 2, Video Part 4 Lecture 3, Video Part 1 \| Lecture 3, Video Part 2 \| Lecture 3, Video Part 3 \| Lecture 3, Video Part 4 Lecture 4, Video Part 1 \| Lecture 4, Video Part 2 \| Lecture 4, Video Part 3 \| Lecture 4, Video Part 4
Neel Krishnaswami	University of Cambridge	Dependent Types and Linearity Lecture 1 notes Lecture 2 notes
Dan Licata	Wesleyan University	Programming Languages Background Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 Lecture 2, Video Part 1 \| Lecture 2, Video Part 2 \| Lecture 2, Video Part 3 \| Lecture 2, Video Part 4 Lecture 3, Video Part 1 \| Lecture 3, Video Part 2 \| Lecture 3, Video Part 3 \| Lecture 3, Video Part 4 Lecture 4, Video Part 1 \| Lecture 4, Video Part 2 \| Lecture 4, Video Part 3 \| Lecture 4, Video Part 4
Frank Pfenning	Carnegie Mellon University	Substructural Type Systems and Concurrent Programming Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 Lecture 2, Video Part 1 \| Lecture 2, Video Part 2 \| Lecture 2, Video Part 3 \| Lecture 2, Video Part 4 Lecture 3, Video Part 1 \| Lecture 3, Video Part 2 \| Lecture 3, Video Part 3 \| Lecture 3, Video Part 4 Lecture 4, Video Part 1 \| Lecture 4, Video Part 2 \| Lecture 4, Video Part 3 \| Lecture 4, Video Part 4 Lecture 5, Video Part 1 \| Lecture 5, Video Part 2 \| Lecture 5, Video Part 3 \| Lecture 5, Video Part 4
Sam Tobin‑Hochstadt	Indiana University	Contracts and Gradual Types Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 Lecture 2, Video Part 1 \| Lecture 2, Video Part 2 \| Lecture 2, Video Part 3 \| Lecture 2, Video Part 4 \| Lecture 2, Video Part 5 Lecture 3, Video Part 1 \| Lecture 3, Video Part 2 \| Lecture 3, Video Part 3 \| Lecture 3, Video Part 4 Lecture 4, Video Part 1 \| Lecture 4, Video Part 2 \| Lecture 4, Video Part 3 \| Lecture 4, Video Part 4
David Van Horn	University of Maryland	Redex, Abstract Machines, and Abstract Interpretation Lecture 1, Video Part 1 \| Lecture 1, Video Part 2 \| Lecture 1, Video Part 3 \| Lecture 1, Video Part 4 Lecture 2, Video Part 1 \| Lecture 2, Video Part 2 \| Lecture 2, Video Part 3 \| Lecture 2, Video Part 4 \| Lecture 2, Video Part 5 Lecture 3, Video Part 1 \| Lecture 3, Video Part 2 \| Lecture 3, Video Part 3 \| Lecture 3, Video Part 4 Lecture 4, Video Part 1 \| Lecture 4, Video Part 2 \| Lecture 4, Video Part 3