ACM SIGPLAN Courses

In-Order Execution Nails Every Weak Memory Behavior

Explore in-order execution's comprehensive coverage of weak memory behaviors, unveiling its significance in modern computing systems.

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

How Do We Know That Weak Memory Matters?

Explore weak memory's impact on system reliability and security, examining evidence and alternative explanations with Mike Dodds.

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

Weak Memory Demands Model-based Compiler Testing

Explore compiler bugs arising from relaxed hardware memory models and their implications for testing, using an LLVM toolchain bug as a case study.

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

Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Models

Explore innovative techniques for validating weak memory persistency models in Non-Volatile Memory, including timing attacks and machine learning approaches to overcome traditional limitations.

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

What We Learned from C++ Atomics and Memory Model Standardization

Explore insights from C++ atomics and memory model standardization, covering usage patterns, performance implications, implementation challenges, and lessons learned in language design.

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

Why Languages Should Preserve Load-Store Order

Explore the complexities of memory models and load-store reordering in programming languages, examining their impact on code optimization and reasoning.

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

On the Need for Available, Functional, and Reusable Memory Models

Explore challenges in memory model research through personal failure stories, highlighting shortcomings and future expectations for the field.

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

Compositional Verification of Concurrent C Programs with Search Structure Templates

Explore compositional verification of concurrent C programs using search structure templates, separating concurrency-control and data-structure components for modular proof combination.

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

Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs

Explore formalization of parallel critical pairs in Isabelle, simplifying definitions and generalizing criteria for confluence and commutation in term rewrite systems.

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

Formalizing the ∞-Categorical Yoneda Lemma

Explore the first formalization of ∞-category theory's Yoneda lemma using Rzk, a new proof assistant for synthetic ∞-category theory, paving the way for advanced mathematical proofs.

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

Lean Formalization of Extended Regular Expression Matching with Lookarounds

Explore a formalized matching algorithm for extended regular expressions using Lean 4, covering intersection, complement, and lookarounds in symbolic derivatives and locations.

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

A Formalization of Complete Discrete Valuation Rings and Local Fields

Explore formalization of complete discrete valuation rings and local fields in Lean, covering theory, proofs, and applications to algebraic number theory and geometry.

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

UTC Time, Formally Verified - Presentation at CPP 2024

Explore formal verification of UTC time conversions using Coq and MathComp, including leap seconds implementation and refinement techniques for software verification projects.

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

Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture

Explore the formalization of Giles Gardam's disproof of Kaplansky's Unit Conjecture using Lean 4, combining deductive proving and verified computation.

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

Univalent Double Categories - Formalization and Applications in Category Theory

Explore univalent double categories in category theory, their formalization in Coq, and applications in mathematics and computer science.

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