University of Oregon University of Oregon

Parallelism and Concurrency

OPLSS 2018 — July 9-21, 2018
Optional Review — July 3-8, 2018

Foundations of Programming Languages - July 3-7

Paul Downen (University of Oregon) and Jan Hoffmann (Carnegie Mellon University) will conduct an introductory session covering the foundations of programming languages (semantics, types, proof techniques, etc.). The introductory session will help attendees who have not taken a course on this material prepare for the rest of the school. Please contact the organizers if you have questions about whether the introduction session will be helpful given your background.

Instructor's Copious Notes | Participant Notes

Day 1

Binding and static scope (Paul Downen)

Alpha-renaming; free and variables; capture avoiding substitution

Static semantics (Jan Hoffmann)

Typing judgment; inference rules; rule induction; inductive definitions

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Dynamic semantics and type safety (Jan Hoffmann)

Structural operational semantics (aka small step); progress and preservation; call-by-name versus call-by-value

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4

Typed and untyped lambda-calculus (Paul Downen)

Alpha-beta-eta laws; evaluation context; Church encodings; Y-combinator and Russell paradox; termination

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3 | Lecture 4, Video Part 4

Day 2

Finite Data Structures (Jan Hoffmann)

Sum types; product types ; option types versus null pointers

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

Recursive Types and programs (Paul Downen)

Godel system T; Peano arithmetic; recursor; iso versus equi-recursive; encodings; typed Y combinator; non-termination)

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Evaluation dynamics and cost semantics (Jan Hoffmann)

PCF;big step operational semantics (aka natural semantics); fixed points recursion; correspondence of cost semantics)

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Day 3

Cost semantics of parallelism (Jan Hoffman)

parallel PCF; parallelism vs concurrency;cost graph; Brent's theorem; work vs depth

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

Parametric Polymorphism (Paul Downen)

System F; polymorphic lambda calculus; type abstraction; generics; universal types; second order propositional logic)

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Encodings of well founded structures (Jan Hoffmann)

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Day 4

Linear Logic (Paul Downen)

Curry-howard (proofs-as-programs);sequent calculus; MALL (Multiplicative Additive Linear Logic); duality theorem; involutive negation; one-sided vs two-sided presentation

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

Linear lambda calculus (Paul Downen)

linear and non-linear; resource safety; pattern-matching

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Day 5

Reducibility - STLC (Paul Downen)

Proof of termination; logical relations; Tait's method; fundamental lemma (adequacy/soundness); term model semantics

Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

Reducility candidates - System F (Paul Downen)

Proof of termination; GIrard's method; parametricity; free theorems

Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3

Main Program: Parallelism and Concurrency - July 9-21

The program consists of 80-minute lectures. Most days, there is also a 80 minute hands-on session for participants to work through exercises given in lecture.

Umut Acar — Carnegie Mellon University

Parallel Algorithms

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 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Lecture 5, Video Part 1 | Lecture 5, Video Part 2 | Lecture 5, Video Part 3 | Lecture 5, Video Part 4

Arvind — Massachusetts Institute of Technology

Dataflow: A Retrospective

Dataflow Publications

Lecture 1, slides | Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

Atomicity in Modular Design

Bluespec Publications

Lecture 2, slides | Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4

Bluespec System Verilog: Concurrency and Semantics

Lecture 3, slides Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Stephanie Balzer — Carnegie Mellon University

Session-Typed Concurrent Programming

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 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Andrej Bauer — University of Ljubljana

Algebraic Effects and Handlers

Resources

Lecture Notes

What is algebraic about algebraic effects and handlers?

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

Designing a programming language

Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Programming with algebraic effects and handlers

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Guy Blelloch — Carnegie Mellon University

Parallel Cost Semantics and Bounded Implementations

Lecture 1, Slides | 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 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Lecture 4, Video Part 1 | Lecture 4, Video Part 2 | Lecture 4, Video Part 3

Lecture 5, Video Part 1 | Lecture 5, Video Part 2 | Lecture 5, Video Part 3

William Duff — JaneStreet

Typing speed: how rich types enable performance engineering

Video Part 1 | Video Part 2

Dan R. Ghica — University of Birmingham

Game Semantics

Lecture 1, Notes | 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 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Robert Harper — Carnegie Mellon University

Computational Type Theory

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 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 5, Video Part 1 | Lecture 5, Video Part 2 | Lecture 5, Video Part 3

Gabriele Keller — University of New South Wales

Purely Functional Array Programming and its Compilation to High-Performance Architectures

Please make sure that you have Haskell and Accelerate installed. Additionally, you should work through the Learning Haskell Tutorial

Parallel Functional Array Programming

Example Haskell programs: EDSL | Deep1 | Deep2 | Deep3 | BlackScholes

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 3, Video Part 1 | Lecture 3, Video Part 2

Keshav Pingali — University of Texas, Austin

Parallel Program = Operator + Schedule + Parallel Data Structures

Lecture 1, slides | Lecture 1, Video Part 1 | Lecture 1, Video Part 2 | Lecture 1, Video Part 3 | Lecture 1, Video Part 4

Lecture 2, slides | Lecture 2, Video Part 1 | Lecture 2, Video Part 2 | Lecture 2, Video Part 3 | Lecture 2, Video Part 4

Lecture 2, slides | Lecture 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3 | Lecture 3, Video Part 4

Lecture 1, slides | Lecture 1, slides

Vijay Saraswat — Goldman Sachs

Resilient X10

X10 Installation Guide

instructions for using the cluster

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 3, Video Part 1 | Lecture 3, Video Part 2 | Lecture 3, Video Part 3

Aaron Turon — Mozilla

Help wanted: research questions in Rust

Blog Posts

Notes | Video Part 1 | Video Part 2 | Video Part 3 | Video Part 4