Oregon Programming Languages Summer School 2013
- Coq Preparation and Boot Camp
- Amal Ahmed Logical Relations
- Robert Harper Type Theory Foundations
- Dan Licata Dependently-Typed Programming in Agda
- Simon Peyton-Jones Adventures in Haskell
- Frank Pfenning Linear Logic and Session-Based Concurrency
- Andrew Tolmach Software Foundations in Coq
- Stephanie Weirich Designing Dependently-Typed Programming Languages
- Steve Zdancewic Verifying LLVM Optimizations in Coq
Oregon Programming Languages Summer School 2012
- Amal Ahmed Logical Relations
- Steve Awodey Category theory Foundations
- Robert Constable Proofs as Processes
- Pierre-Louis Curien Polarization and Focalization
- Robert Harper Type Theory Foundations
- John Hughes Monads and All That
- Xavier Leroy Compiler Verification
- Andrew Myers Language-Based Security
- Frank Pfenning Proof Theory Foundations
- Benjamin Pierce Software foundations in Coq
Oregon Programming Languages Summer School 2011
- Amal Ahmed Logical Relations
- Nick Benton Monadic Effects
- Robert Constable Polymorphic Logic
- Pierre-Louis Curien Polarisation and Focusing
- Robert Harper Type Theory Foundation
- Hugo Herbelin The Calculus of Inductive Constructions
- Xavier Leroy Compiler Certification
- Paul-André Melliès Programming Languages in String Diagrams
- Greg Morrisett Imperative Programming in Coq
- Frank Pfenning Proof Theory Foundation
- Benjamin Pierce Proof Theory in Coq
- Dana Scott Semilattices, Domains, and Computability
- Brent Yorgey Coq Labs
- Dana Scott What is a Proof? Some Challenges for Automated Theorem Proving
- John Harrison Formal Verification in Industry
- Robert Constable Design Issues for Implemented Type Theories