Each year, the Oregon Programming Language Summer School covers topics in the foundations of programming languages. All the recordings of the lectures that took place during this year's event are now available online for free.

ACM SigPlan inaugurated the Oregon Programming Language Summer School, or OPLSS for short, in 2002 and since then it has been repeated every year during the summer. It's interesting to look at the topics through the years:

2002 — Proofs as Programs
2003 — Foundations of Security
2004 — Software Security
2005 — Reliable Computing
2006 — Concurrent and Distributed Software
2007 — Integrating with the External World
2008 — Logic and Theorem Proving
2009 — Theory & Practice of Language Implementation
2010 — Logic, Languages, Compilation, and Verification
2011 — Types, Semantics and Verification
2012 — Logic, Languages, Compilation, and Verification
2013 — Types Logic, and Verification
2014 — Types, Logic, Semantics, and Verification
2015 — Types, Logic, Semantics, and Verification
2016 — Types, Logic, Semantics, and Verification
2017 — A Spectrum of Types
2018 — Parallelism and Concurrency
2019 — Foundations of Probabilistic Programming and Security
2021 — Foundations of Programming and Security
2022 — Types, Semantics, and Program Reasoning
2023 — Types, Semantics, and Logic

This year's topic was "Types, Semantics, and Applications" and the event was hosted by Boston University.

Of course, from that list you can derive that the conference looks at things from a purely theoretical and conceptual perspective. For instance how does "Semantic Type Soundness and Language Interoperability" sound like? Exactly. And don't be fooled by the "Applications" part in "Types, Semantics, and Applications"; it refers to the applications of probabilistic programming languages and a few exercises based on Coq.

Although there's almost 40 recordings, the number of lectures they relate to is 9, as some had no recordings. So the ones with a recording are:

Semantic Type Soundness and Language Interoperability
This lecture covers the use of logical relations to prove semantic type soundness of programming languages with increasingly advanced features and then show how a twist on the same technique can be can be employed to verify the soundness of foreign-function interfaces and language interoperability.

Rule-based languages: from modular design to modular verification
Everything you ever wanted to learn about Rule-based hardware languages, like Bluespec and their use of atomic rules, a nonstructural method of composition which embodies communication protocols between modules.

Language-Based Security
This surveys topics in Language-Based Security, including information-flow control, reasoning about cryptographic protocols, enforcing language abstractions, and more.

Foundations of Programming Languages
Most interesting. We use programming languages to precisely define our programs, what they should do, and how they should operate. But how do we define a programming language itself?

Probabilistic Programming from the Ground Up
What are the principles for designing scalable systems and tools to aid in the development, verification, and application of probabilistic uncertainty across today's software stack?

Adjoint Functional Programming
Looks into the fundamental notions of functional programming from proof theory, like cut elimination, polarity, focusing, and linearity and relate them throughout to advanced concepts in modern programming languages.

Program Analysis with Kleene Algebra with Tests
The lecture provides an overview of Kleene Algebra with Tests test framework, including the syntax, semantics, and the coalgebraic theory underlying decision procedures for program equivalence

The Real/Ideal Paradigm
This introduces participants to the real/ideal paradigm of theoretical cryptography, which is also known as simulation-based security.

Formal Verification of Monadic Computations
This looks at an approach to specifying, implementing, and testing the behaviors of interactive systems.

From all those, I as a practitioner could relate the most with "Foundations of Programming Languages" which although very theoretical in nature, introduces the common tools and techniques that we use to understand and prove properties about programs, the languages we use to express them, and the implementations of those languages. Topics include type safety, polymorphism and modularity, program equality, and computational effects and more.

While the material is written primarily for graduate students, the school is also attended by undergrads, professors and industry professionals too like those from Google and Amazon.

Ultimately, OPLSS devotes itself to teaching the principles of programming languages to students and professionals, breeding the next generation of programming languages' creators.

More Information

Summer 2024 Main site

Summer 2024 Complete Program on Youtube

Related Articles

Carnegie Mellon Principles of Functional Programming

Take Harvard's CS50 Introduction to Artificial Intelligence with Python For Free

To be informed about new articles on I Programmer, sign up for our weekly newsletter, subscribe to the RSS feed and follow us on Twitter, Facebook or Linkedin.

Comments

Make a Comment or View Existing Comments Using Disqus

or email your comment to: comments@i-programmer.info