ACM SIGPLAN Courses

Effective Sequential Monte Carlo for Language Model Probabilistic Programs

Explore efficient Sequential Monte Carlo for language model probabilistic programs. Learn about LLaMPPL library, design challenges, and outperforming state-of-the-art LLMs on various tasks.

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

Toward Probabilistic Coarse-to-Fine Program Synthesis

Explore probabilistic coarse-to-fine program synthesis, a novel approach using iterative refinement of stochastic programs to efficiently search and generate programs matching specifications.

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

Abstract Interpretation for Automatic Differentiation

Explore abstract interpretation for automatic differentiation, analyzing its application in machine learning, scientific computing, and graphics.

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

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving

Explore a novel approach for deriving guaranteed bounds on normalized posterior distributions in probabilistic programs using polynomial solving techniques.

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

Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions - LAFI'24

Explore a technique for finding guaranteed bounds on posterior distributions in probabilistic programs with loops using probability generating functions and inductive invariants.

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

Effect Handlers for Choice-Based Learning in Machine Learning Programming

Explore a novel choice-based learning paradigm combining algebraic effects, handlers, and loss continuations to enhance modularity in machine learning programming.

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

Evolving Weak Memory Models for Evolving Architectures

Explore evolving weak memory models for modern architectures, focusing on advancements and challenges in concurrent programming and hardware design.

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

What Compilers Desire from Weak Memory Semantics

Explore compiler optimization challenges in concurrent programs, focusing on memory models and safety. Investigate deriving models that retain optimization safety across different consistency levels.

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

System-Level Weak Memory Models: The Need for Formalisation, ISA Semantics Integration and Model Diversity

Explore system-level weak memory models, focusing on formalization, ISA semantics integration, and model diversity in computer architecture.

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

Programmers Love Mind-Bogglingly Complicated Weak Memory Models

Explore mind-boggling complexities of weak memory models in programming, delving into their intricacies and implications for software development.

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

Later Credits: A Case Study in the Unreasonable Effectiveness of Separation Logic

Explore the effectiveness of separation logic in software verification through a case study on "Later Credits" presented by Derek Dreyer.

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

Designing Wait-free Weak Reference Counting

Explore wait-free weak reference counting design techniques for efficient memory management in concurrent systems.

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

Lifting Compiler Security Properties to Stronger Attackers: The Speculation Case

Explore compiler security properties against speculative execution attacks, focusing on lifting guarantees to stronger attacker models and developing a formal framework for well-formedness conditions.

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

Domesticating Automation for Large-Scale Verification Systems - Dafny'24

Explore automated theorem proving's potential for scaling verification-based development, focusing on user experience and efficient automation budget management in large-scale systems.

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

Verifying Dafny Contract Integrity - Detecting Common Pitfalls

Detect and prevent common pitfalls in Dafny contracts, including contradictions, vacuity, unconstrained outputs, and redundancy. Enhance software specification accuracy.

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