ACM SIGPLAN Courses

Reference Capabilities for Flexible Memory Management

Explore Verona's innovative approach to memory management using isolated regions and reference capabilities, enabling predictable and controlled memory use in concurrent programming.

• YouTube
• 18 minutes
• Self-Paced
• Free Video

Mutually Iso-Recursive Subtyping - OOPSLA 2023

Explore mutually iso-recursive subtyping, addressing challenges in type recursion for programming languages. Gain insights into efficient type checking and subtyping for intermediate code representations.

• YouTube
• 19 minutes
• Self-Paced
• Free Video

Type-Safe Dynamic Placement with First-Class Placed Values

Explore type-safe dynamic placement in distributed systems using first-class placed values. Learn about Dyno, a language enabling static reasoning with dynamic placement flexibility.

• YouTube
• 16 minutes
• Self-Paced
• Free Video

Optimization-Aware Compiler-Level Event Profiling

Explore a novel technique for quantifying compiler-internal events in optimized code, reducing profiling perturbation and enhancing dynamic analysis accuracy.

• YouTube
• 19 minutes
• Self-Paced
• Free Video

Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols

Explore a novel interactive verification methodology using relational abstraction to tackle quantifier reasoning challenges in infinite-state systems, with applications to distributed protocols.

• YouTube
• 16 minutes
• Self-Paced
• Free Video

MemPerf: Profiling Allocator-Induced Performance Slowdowns

Explore MemPerf, a novel profiler for identifying allocator-induced performance slowdowns. Learn about life-cycle based detection, thread-aware modeling, and unified methods for pinpointing memory access issues.

• YouTube
• 19 minutes
• Self-Paced
• Free Video

Verus: Verifying Rust Programs Using Linear Ghost Types

Explore Verus, an SMT-based tool for formally verifying Rust programs. Learn how it leverages Rust's linear types and borrow checking to prove functional correctness in low-level, high-assurance systems.

• YouTube
• 18 minutes
• Self-Paced
• Free Video

Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems

Explore efficient Boolean unification for Hindley-Milner-style type and effect systems. Learn about a hybrid algorithm improving compilation speed and reducing inference overhead in polymorphic effect systems.

• YouTube
• 18 minutes
• Self-Paced
• Free Video

Synthesizing Precise Static Analyzers for Automatic Differentiation

Explore Pasado, a technique for synthesizing precise static analyzers for Automatic Differentiation, improving precision in nonlinear operations and demonstrating applications in various domains.

• YouTube
• 17 minutes
• Self-Paced
• Free Video

Automated Translation of Functional Big Data Queries to SQL

Explore automated translation of functional big data queries to SQL, improving efficiency while maintaining abstraction benefits. Learn about novel column-wise decomposition for query synthesis.

• YouTube
• 14 minutes
• Self-Paced
• Free Video

A Pretty Expressive Printer - An Optimal and Flexible Approach to Document Layout

Explore a novel pretty printer that maximizes expressiveness, optimality, and performance. Learn about its unique features, formal verification, and real-world application in Racket code formatting.

• YouTube
• 17 minutes
• Self-Paced
• Free Video

Formal Abstractions for Packet Scheduling

Explore formal abstractions for packet scheduling in software-defined networking, focusing on PIFO trees' syntax, semantics, and compilation algorithms for optimizing network performance.

• YouTube
• 17 minutes
• Self-Paced
• Free Video

Translating Canonical SQL to Imperative Code in Coq

Explore a mechanically verified compiler translating SQL to imperative code, addressing implementation challenges and leveraging formalization advances in query compilation.

• YouTube
• 18 minutes
• Self-Paced
• Free Video

Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid

Explore Mat2Stencil, a novel domain-specific language for PDE solvers on structured grids. Learn about its matrix abstraction, compiler, and automatic parallelization techniques for efficient implementation.

• YouTube
• 15 minutes
• Self-Paced
• Free Video

Languages with Decidable Learning: A Meta-theorem

Explore finite-aspect checkable languages and their role in decidable learning, connecting expression syntax tree evaluation to finite tree automata for new learning results.

• YouTube
• 18 minutes
• Self-Paced
• Free Video