Nada Amin — Harvard University

Metaprogramming

Lecture 1 video part 1 | part 2 | part 3 | notes

Lecture 2 video part 1 | part 2 | part 3 | notes

Lecture 3 video part 1 | part 2 | part 3 | notes

Roberto Di Cosmo

Software Heritage: Towards A New Era for Software Engineering and AI

Open Source is at the heart of our digital society and embodies a growing part of our technical and organisational knowledge. It speeds up innovation, but also raises key challenges about the quality, evolution and security of the many components that are put together in modern software systems: how to be sure that the source code of a key module we use will be still there when we need it in the future? Do we really know what source code we are using, and where it comes from? Can software engineering studies take advantage from, and improve the quality of the massive amount of information that is available about hundreds of millions of software projects worldwide?

With the AI tidal wave, (open source) software has become not only essential to build new LLMs, but also a precious training dataset that plays a key role in the quality of these models. What are the challenges and opportunities that arise?

In this talk we will present an update on Software Heritage, a groundbreaking non profit initiative launched by Inria in 2016 in partnership with UNESCO to collect, preserve and share all publicly available software in source code form. Software Heritage has already built the largest public archive, with more than 24 billion files from more than 375 million software origins, collected from more than 5000 different code hosting and distribution platforms.

After ten years of work, we show concrete examples of how this is much more than an archive: it is the Very Large Telescope that we need to explore the galaxy of software development at a global scale. With the recent launch of the CodeCommons project, we can work together to tackle all of the above challenges much better than before.

Lecture 1 video part 1 | part 2 | part 3

Limin Jia — Carnegie Mellon University

Information Flow Type Systems

Lecture 1 video part 1 | part 2 | part 3 | notes

Lecture 2 video part 1 | part 2 | part 3 | notes

Lecture 3 video part 1 | part 2 | part 3 | notes

Kathryn S McKinley — Google

Better Computing Culture with a Research Mindset = More Innovation

Adopting a Research Mindset

Lecture 1 part 1 | part 2 | part 3 | slides | notes

Lecture 2 part 1 | part 2 | part 3 | slides | notes

Anja Petković Komel — TU Wien / Argot Collective

Introduction to Type Theories

My lectures are loosely based on the Introduction to Martin-Löf Type Theory in Egbert Rijke's book. We will apply those principles using the Rocq Theorem Prover with VS Code, but Rocq ships with RocqIDE, so also you can use emacs, vim or RocqIDE as editors.

MLTT | Rcoq Intro

Lecture 1 part 1 | part 2 | part 3 | slides | notes

Lecture 2 video part 1 | part 2 | part 3 | notes | Identity Type Two-sided MLTT

Lecture 3 video part 1 | part 2 | part 3 | notes

Lecture 4 video part 1 | part 2 | part 3

Lecture 5 video part 1 | part 2 | part 3 | Rcoq Examples | notes

Emina Torlak — Amazon Web Services

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization

The instructions for installing Cedar are here. For the lectures, you should also clone this repo, as it contains the sample code we will be using. The easiest way to edit code in Cedar is through VSCode with the "Cedar" extension.

Lecture 1 video part 1 | part 2 | part 3

Jeannette Wing — Columbia University

Trustworthy AI

slides | notes | article: Trustworthy AI

Niki Vazou — IMDEA Software Institute

Refinements Types Contributed Lecture