ACM SIGPLAN Courses

Lower Bounds for Possibly Divergent Probabilistic Programs

Explore a new proof rule for verifying lower bounds on quantities of probabilistic programs, applicable to possibly divergent programs and non-trivial cases like three-dimensional random walks.

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

Continuing WebAssembly with Effect Handlers

Explore WasmFX, an extension to WebAssembly enabling direct translation of non-local control features via effect handlers, improving compiler efficiency for various programming languages.

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

Building Dynamic System Call Sandbox with Partial Order Analysis

Explore dynamic system call sandboxing using partial order analysis to enhance OS security. Learn how to restrict unnecessary system calls and reduce attack surfaces in program execution.

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

Fluent APIs in Functional Languages

Explore implementing fluent APIs in functional languages using parametric polymorphism and Hindley-Milner type inference. Learn to enforce API protocols and DSL syntax at compile time without relying on name overloading.

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

P4R-Type: A Verified API for P4 Control Plane Programs

Explore P4R-Type, a verified API for P4 control plane programs, enhancing safety in Software-Defined Networking. Learn about static checks and formal foundations to prevent catastrophic failures in network programming.

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

Static Analysis of Memory Models for SMT Encodings

Improve efficiency of bounded model checkers with static analysis and SMT encoding optimizations for memory models, reducing verification time by up to 40% in challenging benchmarks.

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

Grounded Copilot - How Programmers Interact with Code-Generating Models

Explore how programmers interact with AI coding assistants like Github Copilot, uncovering bimodal usage patterns and providing recommendations for future AI programming tools.

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

How Profilers Can Help Navigate Type Migration

Explore strategies for guiding migratory typing using profiling tools, focusing on deep types to eliminate costly boundaries between typed and untyped components in code refactoring.

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

Verifying Indistinguishability of Privacy-Preserving Protocols

Explore a novel approach to verifying privacy-preserving protocols, balancing precision and accessibility. Learn about indistinguishability proofs and their application to TLS and PIR protocols.

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

Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts

Explore automated synthesis of parametric gas upper-bounds for smart contracts using novel geometric approaches, enhancing blockchain security and efficiency.

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

Melocoton - A Program Logic for Verified Interoperability Between OCaml and C

Explore Melocoton, a groundbreaking program logic for verifying interactions between OCaml and C components through OCaml's foreign function interface, featuring a formal semantics and Coq mechanization.

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

Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs

Explore a novel methodology for sampling datasets to train neural network-based program surrogates, focusing on complexity-guided sampling for improved accuracy in real-world applications.

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

Simple Reference Immutability for System F-sub

Explore reference immutability in hybrid languages, focusing on interactions with higher-order functions, polymorphism, and subtyping in System F-sub. Gain insights into taming mutation in modern programming paradigms.

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

A Grounded Conceptual Model for Ownership Types in Rust

Explore a systematic approach to teaching Rust's ownership types, featuring a new assessment tool, conceptual model, and visualizations to improve learner understanding of memory safety concepts.

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

Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection

Explore a novel framework for modular specification of distributed protocols using hybrid multiparty session types, enabling compositionality while preserving semantic guarantees.

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