OPLSS 2012 by Robert Harper.
From the post:
The 2012 edition of the Oregon Programming Languages Summer School was another huge success, drawing a capacity crowd of 100 eager students anxious to learn the latest ideas from an impressive slate of speakers. This year, as last year, the focus was on languages, logic, and verification, from both a theoretical and a practical perspective. The students have a wide range of backgrounds, some already experts in many of the topics of the school, others with little or no prior experience with logic or semantics. Surprisingly, a large percentage (well more than half, perhaps as many as three quarters) had some experience using Coq, a large uptick from previous years. This seems to represent a generational shift—whereas such topics were even relatively recently seen as the province of a few zealots out in left field, nowadays students seem to accept the basic principles of functional programming, type theory, and verification as a given. It’s a victory for the field, and extremely gratifying for those of us who have been pressing forward with these ideas for decades despite resistance from the great unwashed. But it’s also bittersweet, because in some ways it’s more fun to be among the very few who have created the future long before it comes to pass. But such are the proceeds of success.
As if a post meriting your attention wasn’t enough, it concludes with:
Videos of the lectures, and course notes provided by the speakers, are all available at the OPLSS 12 web site.
Just a summary of what you will find:
- Logical relations — Amal Ahmed
- Category theory foundations — Steve Awodey
- Proofs as Processes — Robert Constable
- Polarization and focalization — Pierre-Louis Curien
- Type theory foundations — Robert Harper
- 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
Enjoy!