ACM SIGPLAN Courses

Retrofitting Null-Safety into Java

Explore Nullsafe, a compiler plugin extending Java's type system with nullness, reducing NullPointerExceptions in production code at Meta through large-scale transformation.

• YouTube
• 36 minutes
• On-Demand
• Free Video

Inside the Scala Capture Checker

Explore Scala's capture checker, its algorithms, architecture, and integration into the compiler for ensuring resource and effect safety in programs.

• YouTube
• 1 hour 3 minutes
• On-Demand
• Free Video

Automatic Parallelism Management - POPL 2024

Explore techniques for automatic parallelism management in high-level languages, combining static and runtime approaches to optimize performance without manual tuning.

• YouTube
• 25 minutes
• On-Demand
• Free Video

The Network is the Computer: A Programming Language Perspective

Explore the convergence of programming languages and networking, examining custom protocols and in-network functionality to gain insights for both fields.

• YouTube
• 1 hour 8 minutes
• On-Demand
• Free Video

Implementation and Synthesis of Math Library Functions

Explore MegaLibm, a domain-specific language for implementing, testing, and tuning math library functions. Learn how it enhances safety, modularity, and tunability in mathematical software development.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Coarser Equivalences for Causal Concurrency

Explore relaxations of trace equivalence in concurrent programs, focusing on grain equivalence for efficient causal concurrency analysis while maintaining algorithmic advantages.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Modular Denotational Semantics for Effects with Guarded Interaction Trees

Explore guarded interaction trees for representing higher-order computations with effects in Coq. Learn about modular reasoning and cross-language interactions in higher-order languages.

• YouTube
• 21 minutes
• On-Demand
• Free Video

Guided Equality Saturation

Explore guided equality saturation, a semi-automatic rewriting technique scaling complex tasks in theorem proving and compilation by incorporating human insight at key decision points.

• YouTube
• 21 minutes
• On-Demand
• Free Video

Capturing Types: A Calculus for Tracking Free Variables in Type Systems

Explore a calculus representing captured variables in types for enhanced safety, enabling effect implementation via scoped capabilities and guiding practical capture checking in programming languages.

• YouTube
• 20 minutes
• On-Demand
• Free Video

A New Perspective on Commutativity in Verification

Explore a fresh perspective on commutativity in program proofs, focusing on its application in automated verification goals for various program types and properties.

• YouTube
• 58 minutes
• On-Demand
• Free Video

Internalizing Indistinguishability with Dependent Types

Explore a novel type system combining dependency tracking and dependent types, internalizing indistinguishability for enhanced information flow control and program equivalence reasoning.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Nominal Recursors as Epi-Recursors - POPL 2024

Explore nominal recursors in syntax with bindings, comparing expressiveness and viewing them as epi-recursors. Develop a framework for comparison and apply to nominal corecursors, validated with Isabelle/HOL.

• YouTube
• 21 minutes
• On-Demand
• Free Video

Monotonicity and the Precision of Program Analysis

Explore the connection between program monotonicity and analysis precision. Learn how monotone behavior enables complete abstract interpretation for numeric invariant inference.

• YouTube
• 21 minutes
• On-Demand
• Free Video

When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism

Explore a novel type inference approach for first-class polymorphism using multi-bounded polymorphism, advancing the state of the art in type inference for programming languages.

• YouTube
• 22 minutes
• On-Demand
• Free Video

Polymorphic Type Inference for Dynamic Languages

Explore a novel type system combining polymorphism, intersection types, and subtyping for dynamic languages. Learn about type reconstruction algorithms and their applications in advanced programming.

• YouTube
• 21 minutes
• On-Demand
• Free Video