ACM SIGPLAN Courses

From Traces to Program Incorrectness: A Type-Theoretic Approach

Explore a type-theoretic framework for reasoning about incorrectness in functional programs interacting with effectful library APIs, using traces represented by symbolic regular expressions for formal specification and analysis.

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

Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms

Explore a novel separation logic approach for automated safety verification of distributed actor systems, focusing on cyclic message histories to enable verification of complex algorithms like Paxos.

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

Enhancing Infer Compositional Analysis with Summary Specialization

Discover how Summary Specialization enhances Infer's compositional reasoning for static analysis, balancing assumptions about call sites without resorting to full global analysis, with experimental results on closure resolution.

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

Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching

Explore Total Outcome Logic, a unified framework for reasoning about program termination and nontermination across different branching effects, including nondeterminism and randomization.

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

U-turn: Forward-driven Backward Analysis for Incorrectness

Explore a novel approach combining forward and backward reasoning for incorrectness logic in static analysis, revealing true bugs and their preconditions while avoiding false alarms.

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

Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation

Discover a logical approach to automatically detect type unsoundness in libraries using unsafe features through under-approximate reasoning and separation logic assertions for scalable bug detection.

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

Proto-Quipper with Reversing and Control

Explore the semantics of reversible and controllable quantum circuits in Proto-Quipper, focusing on the formalization of operations like reversing, control, and with-computed through categorical models and type systems with modalities.

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

Towards Generic Higher-Order Unification Implementations in Haskell

Explore the development of generic higher-order unification algorithms in Haskell using Free Foil library, extending it with parametrised metavariables to implement Huet's preunification and Miller's pattern unification algorithms.

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

The Quantum Abstract Machine

Explore the Quantum Abstract Machine (QAM) model designed to support abstract yet accurate design and verification of quantum communication protocols, accessible to non-specialists while maintaining quantum accuracy.

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

QuteFuzz: Fuzzing Quantum Compilers Using Randomly Generated Circuits with Control Flow and Subcircuits

Discover QuteFuzz, a tool for detecting quantum compiler bugs by generating random quantum programs with higher-level abstractions, revealing 17 bugs in major quantum software stacks like Pytket, Qiskit, and Cirq.

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

All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants

Explore sort polymorphism for proof assistants like Coq, Lean, and Agda, addressing limitations in current approaches and enabling better reuse across different universe sorts in dependent type theory.

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

Program Analysis via Multiple Context Free Language Reachability

Explore Multiple Context Free Language (MCFL) reachability as a new approach for static program analysis, offering tunable precision while maintaining tractability for approximating interleaved Dyck reachability problems.

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

Coinductive Proofs for Temporal Hyperliveness

Explore coinductive proof techniques for temporal hyperproperties, focusing on approximating hyperliveness properties through coinductive relations and implementing them in the HyCo framework within Coq.

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

Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops

Discover novel approaches for bounding posterior distributions of discrete probabilistic programs with loops through residual mass semantics and geometric bound semantics, with automated implementation in Diabolo.

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

Consistency of a Dependent Calculus of Indistinguishability

Explore the logical consistency, normalization, and decidable type conversion of DCOIω, a dependent calculus that enables proof irrelevance through indistinguishability and dependency tracking.

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