OPLSS 2025 Topics | University of Oregon

The program consists of 80-minute lectures.

Nada Amin — Harvard University

Metaprogramming

Valeria De Paiva — Topos Institute

Lambda-Calculi for Logics

Formal Methods for National Security

Limin Jia — Carnegie Mellon University

Information Flow Type Systems

Delia Kesner — Université Paris Cité

Lambdi Calculi through the Lens of Linear Logic

System Design and Innovation: A Garbage Collection Case Study

Anja Petković Komel — TU Wien / Argot Collective

Introduction to Type Theories

We will use the Rocq Theorem Prover with VS Code, but Rocq ships with RocqIDE, or you can use emacs or vim as editors.

Brigitte Pientka — McGill University

Introduction to Logical Foundations

(aka the beauty of the Curry-Howard Isomorphism at play)

Paige Randall North — Utrecht University

Introduction to Category Theory

Emina Torlak — Amazon Web Services

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

Abstract Interpretation-Based Static Analysis

Niki Vazou — IMDEA Software Institute

Refinements Types

Jeannette Wing — Columbia University

Trustworthy AI

Ningning Xie — University of Toronto

Algebraic Effects and Handlers

Oregon Programming Languages Summer School