Nomadic Labs PhD student Colin Gonzalez attended the Oregon Programming Language Summer School, that had the Tezos Foundation as a sponsor in 2022. In this blog post he reflects on his experiences.
One of the perks of preparing a PhD is that sometimes you get to travel to conferences or summer schools. A summer school is like a summer camp where the main activity is attending lectures with fellow grad students from around the world. And on your free time you gather with people to grab a couple of drinks and discuss the lectures but also your own PhD experience. I recently got to attend this year’s edition of Oregon Programming Language Summer School in Eugene, OR.
OPLSS usually lasts two weeks. The first one covers a set of introductory courses on proof theory, type theory and logic; the second week, selected lecturers among the top researchers in the programming languages field are invited to discuss more advanced topics in a privileged setting where students and lecturers share the campus in very casual fashion. This creates opportunities for great discussions over dinner and lunch.
The first few days were rhythmed by a combination of proof theory by Frank Pfenning, type theory by Thorsten Altenkirch, algebraic programming by Jeremy Gibbons and game semantics by Pierre-Louis Curien. Eventually the week closed with a great course on classical realizability by Paul Downen and rewriting theory with Sylvia Ghilezan.
Admittedly, one of the most difficult lectures was the one on Game Semantics. A lecture during which you would glance at your neighbour with a puzzling face and asking quietly: “Do you understand anything?”. The answer would often be just “No” and the same puzzling face. It was for most of us a new topic.
All these topics, either new or a refresh, were a great preparation for the hours we would spend with Robert Harper discussing Logical Relations or implementing a dependent-type theory type-checker with Stephanie Weirich. Also, it was the opportunity to have Stephanie Balzer walking us through the world of Pi-Calculus and Session Types and hearing Adam Chlipala explain how to use a proof assistant like Coq to certify production grade software and hardware. Finally the lectures of Sam Lindley and Steve Zdancevic were a great pair talking respectively of effect handlers and using the free monad in DeepSpec to formalise and verify imperative programs.
I noticed that the lecturers kept connecting Call-by-Push-Value[1] with linear logic and type-theory. Call-by-Push-Value, CBPV for short, which plays a central role in my PhD research, happens to be a very active topic in the US, and it was a pleasant surprise to get so much new insight into this domain during the conference. CBPV is a formalisation of the connection between values and computations. It was an amazing time to get a new perspective on my work.
We can observe this duality when comparing OCaml and Haskell. While
they share similar semantics and features, they differ in the way they
treat values. We could say that in Haskell, every program is a value
in its own right. Whereas in OCaml, values are programs that are in a
special form that can’t be reduced any further. Take for instance the
very short OCaml program (fun x -> x) (1 + 1): OCaml will first
replace 1 + 1 with the value 2, before handing it to the function,
while Haskell would happily pass (1 + 1) as an unevaluated argument
to the function. Eventually, they both give the same result. But this
tiny difference has important implications: OCaml and Haskell programs
do not behave the same because computations happen in different
orders. And this is where CBPV shines: it can be seen as a core
language capable of interpreting both OCaml and Haskell programs correctly.
And the obvious question arises: why is CBPV of interest while doing a PhD at Nomadic Labs? In my PhD, I work on compiling spreadsheets, considered as programs, to Michelson smart contracts, and I use CBPV as a formal framework to reason about the semantics of these programs.
Overall, OPLSS 2022 was a great experience. I got to enjoy some of the best CS lectures I have ever attended, and I gained new perspectives and insight on my own work.
[1]Paul Blain Levy. 1999. Call-by-Push-Value: A Subsuming Paradigm.