Watch The Oregon Programming Language Summer School Lectures
Written by Nikos Vaggalis
Friday, 20 September 2024
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.
A repository containing any PostgreSQL extension you can imagine for Linux distributions is something that might be valuable if you are trying to save some time.
Google has announced an updated version of Gemini, saying that Gemini 2.0 Flash Experimental will "enable even more immersive and interactive applications", along with new coding agents that can take [ ... ]
