University of Oregon University of Oregon

A Spectrum of Types

June 26-July 8, 2017

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:

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

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