University of Oregon

Oregon Programming Languages Summer School — July 16-28, 2012

Logic, Languages, Compilation, and Verification

The program consists of 80 minute lectures presented by internationally recognized leaders in programming languages and formal reasoning research.

Technical Lectures

Logical relations — Amal Ahmed

Category theory foundations — Steve Awodey

Lecture Notes

Proofs as Processes — Robert Constable

Polarization and focalization — Pierre-Louis Curien

Type theory foundations — Robert Harper

Students should be familiar with Nordstroem, Petersson, and Smith. Programming in Martin-Loef's Type Theory.
Additionally, students might consider reading:

Monads and all that — John Hughes

Compiler verification — Xavier Leroy

Language-based security — Andrew Myers

Proof theory foundations — Frank Pfenning

Software foundations in Coq — Benjamin Pierce

Copyright © University of Oregon Department of Computer and Information Science. All rights reserved.
Privacy Policy