ACM SIGPLAN Courses

asai: A Library for Compiler Diagnostics

Explore asai, an OCaml library for enhancing compiler diagnostics in proof assistants, improving error messages for end users.

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

Implementing Separation Logic Using an SMT-backed Frame Rule

Explore implementing separation logic with SMT-backed Frame Rule for symbolic execution. Learn to simplify verification of programs with pointers using CVC5 solver's decidable fragment support.

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

Efficient Evaluation with Controlled Definition Unfolding - WITS'24

Explore efficient evaluation techniques in polymorphic and dependently typed languages, focusing on controlled definition unfolding for improved user interaction and unification processes.

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

Binding Syntax for Dependently-Typed Programs - WITS'24

Explore innovative binding syntax for dependently-typed programs, enhancing ergonomics while maintaining fixed grammar for improved error messaging.

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

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