ACM SIGPLAN Courses

A Gradual Probabilistic Lambda Calculus

Explore a gradual probabilistic lambda calculus combining static and dynamic typing for probabilistic programming, enhancing flexibility in machine learning and differential privacy applications.

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

The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog

Explore a novel approach to Verilog's formal semantics using λV, a core language addressing semantic pitfalls and facilitating tool development for hardware description languages.

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

Towards Better Semantics Exploration for Browser Fuzzing

Explore innovative browser fuzzing techniques using production-context sensitive grammars for enhanced semantic coverage and bug detection in Chrome, Safari, and Firefox.

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

Reusing Just-in-Time Compiled Code - OOPSLA 2023

Explore innovative techniques for reusing compiled code across program runs, reducing warm-up costs in dynamic languages through speculative contextual dispatch and off-line curated code repositories.

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

Perception Contracts for Safety of ML-Enabled Systems

Explore perception contracts for ML-enabled systems safety, focusing on error handling in ground-truth estimations and symbolic learning algorithms for vision-based control systems.

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

Solving Conditional Linear Recurrences for Program Verification: The Periodic Case

Explore a novel approach to solving conditional linear recurrences in program verification, focusing on ultimately periodic index sequences and their closed-form solutions.

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

Gradual Typing for Effect Handlers

Explore gradual typing for effect handlers, integrating effect typing with existing languages. Learn about GrEff language, its semantics, and the graduality theorem through operational logical relations models.

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

Run-Time Prevention of Software Integration Failures of Machine Learning APIs

Explore run-time prevention of ML API integration failures. Learn about SmartGear, a tool detecting and converting mismatching outputs to prevent software incompatibilities.

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

Stuttering for Free - A New Approach to Simulation Proofs

Explore a new simulation technique, FreeSim, for proving behavioral refinements between transition systems, offering simplified meta-theory and enhanced flexibility in verification processes.

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

Adventure of a Lifetime: Extract Method Refactoring for Rust

Explore automated 'Extract Method' refactoring for Rust, addressing ownership and lifetime challenges through program transformations and repair procedures. Gain insights into advanced code refactoring techniques.

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

Hardware-Aware Static Optimization of Hyperdimensional Computations

Explore hardware-aware static optimization for hyperdimensional computing, focusing on minimizing resource usage while meeting accuracy targets in error-prone hardware platforms.

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

Historia: Refuting Callback Reachability with Message-History Logics

Explore a novel approach to callback reachability in event-driven frameworks using message-history logics. Learn about targeted specification and goal-directed verification for improved app analysis.

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

A Deductive Verification Infrastructure for Probabilistic Programs

Explore a novel deductive verification infrastructure for probabilistic programs, featuring an intermediate verification language and real-valued logic for quantitative property verification.

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

Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

Explore a method for generating proof certificates in language-agnostic program verification, enhancing reliability across imperative, functional, and assembly languages.

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

Formally Verifying Optimizations with Block Simulations

Explore formal verification of compiler optimizations using block simulations. Learn about enhancing CompCert with efficient, verified validators for advanced optimizations like LCM and SR.

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