OPLSS 2018 Topics | University of Oregon

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