ACM SIGPLAN Courses

Explainable Program Synthesis by Localizing Specifications

Explore explainable program synthesis through subspecifications, enhancing implementation understanding with logical formulas. Learn algorithms for constructing and verifying subspecifications, their properties, and impact on code comprehension.

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

Interactive Debugging of Datalog Programs

Explore interactive debugging techniques for Datalog programs using a top-down evaluation strategy. Learn about small-step operational semantics and efficient step-over interactions for complex programming tasks.

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

Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning

Explore Outcome Logic, a unified theory for correctness and incorrectness reasoning in program logics, generalizing Hoare Logic to capture computational effects and reachability.

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

A Cocktail Approach to Practical Call Graph Construction

Explore a novel cocktail approach for efficient call graph construction in C-based software, improving precision and scalability for vulnerability detection and code understanding.

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

Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects

Explore bidirectional object-oriented programming for programmatic and direct object manipulation, focusing on a novel language extension and its application in HTML document generation through GUI design.

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

Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs

Explore algebro-geometric algorithms for template-based synthesis of polynomial programs, offering a scalable approach to program sketching without sacrificing completeness.

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

Compiling Structured Tensor Algebra

Explore StructTensor, a framework for symbolically computing tensor structure at compile-time, enhancing efficiency in data-intensive workloads across computational domains.

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

AST vs. Bytecode: Interpreters in the Age of Meta-Compilation

Explore the performance trade-offs between AST and bytecode interpreters in meta-compilation systems. Gain insights into interpreter efficiency, memory usage, and engineering considerations for language implementations.

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

Structural Subtyping as Parametric Polymorphism

Explore the relationship between structural subtyping and parametric polymorphism in programming languages, focusing on their expressive power and potential encodings.

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

Proof Automation for Linearizability in Separation Logic

Explore proof automation for linearizability in separation logic, enhancing verification of fine-grained concurrent programs through innovative proof rules and search strategies.

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

Deep Learning Robustness Verification for Few-Pixel Attacks

Explore a novel L0 robustness verifier for neural networks, addressing few-pixel attacks through dynamic programming, sampling, and covering designs to enhance verification efficiency.

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

Regular Expression Matching using Bit Vector Automata

Explore a new algorithm for efficient regex matching with bounded repetition using nondeterministic bit vector automata, offering improved performance for challenging patterns in practice.

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

Live Pattern Matching with Typed Holes

Explore live pattern matching with typed holes in functional programming, covering static reasoning, live evaluation, and implementation in Hazel for maximally live feedback during coding.

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

Aliasing Limits on Translating C to Safe Rust

Explore limitations and improvements in translating C to safe Rust, focusing on pointer conversion challenges and proposing methods to enhance translation effectiveness.

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

Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable - OOPSLA 2023

Explore a novel graph IR for aggressive global optimizations in impure higher-order languages, combining reachability types and effect systems for precise dependency tracking and efficient code optimization.

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