ACM SIGPLAN Courses

Generically Automating Separation Logic by Functors, Homomorphisms, and Modules

Explore a novel theory for automating Separation Logic using abstract algebras, enabling generic reasoning about complex data structures with compositional instantiation and comparable performance to specialized systems.

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

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus

Explore the decidability of reachability problems in finitary PCF extensions, with focus on undecidability proofs and a novel decidable fragment featuring higher-order recursive functions with reference cells.

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

VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems

Explore VeriRT, an end-to-end formal verification framework that bridges the gap between abstract specifications and implementations for safety-critical real-time distributed systems, with case studies and Coq formalization.

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

Modelling Recursion and Probabilistic Choice in Guarded Type Theory

Explore how guarded type theory can model programming languages with recursion and probabilistic choice, demonstrating both operational and denotational semantics for reasoning about program equivalence.

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

A Verified Foreign Function Interface Between Coq and C

Discover how VeriFFI enables seamless integration between Coq and C programs with guaranteed type safety and correctness, using a hybrid deep/shallow description of Coq dependent types.

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

Bidirectional Higher-Rank Polymorphism with Intersection and Union Types

Explore bidirectional higher-rank polymorphic type inference with intersection and union types, examining theoretical foundations and practical implementations formalized in Coq for modern programming languages.

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

Preservation of Speculative Constant-Time by Compilation - POPL 2025

Explore how compilers can preserve speculative constant-time policies to protect against Spectre-v1 attacks, with examples of failures in GCC and Jasmin, and solutions using formal verification.

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

Derivative-Guided Symbolic Execution

Explore a novel symbolic execution approach for functional programs interacting with effectful libraries, using LTLf specifications and symbolic derivatives to efficiently falsify complex data structure safety properties.

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

Fulminate: Testing CN Separation-Logic Specifications in C

Discover how Fulminate enables runtime testing of separation-logic specifications in C code, demonstrating practical ownership checking on complex examples including a production hypervisor allocator.

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

The Decision Problem for Regular First Order Theories

Explore the extension of the Entscheidungsproblem to regular first-order theories, examining which decidable classes become undecidable and identifying subclasses that remain decidable in this context.

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

Reachability Analysis of the Domain Name System

Explore the first decision procedure for DNS verification, establishing its 2ExpTime complexity through formal semantics, algebraic abstraction, and novel bisimulation techniques for analyzing security vulnerabilities.

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

Adversities in Abstract Interpretation - Accommodating Robustness by Abstract Interpretation

Explore the challenges of abstract interpretation and how robustness can be accommodated through this technique in program analysis.

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

A Quantitative Probabilistic Relational Hoare Logic

Explore eRHL, a groundbreaking program logic for relational expectation properties in probabilistic programs, offering soundness and completeness for program equivalence, statistical distance, and differential privacy.

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

MimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age

Explore MimIR, an extensible intermediate representation for domain-specific languages that enables type-safe compiler optimization without reinventing the wheel, demonstrated through case studies in regular expressions and linear algebra.

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

Auditing Rust Crates Effectively

Discover Cargo Scan, an interactive tool that helps developers audit third-party Rust code by analyzing potentially dangerous side-effects, reducing manual inspection burden and pinpointing security vulnerabilities missed in manual audits.

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