ACM SIGPLAN Courses

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

Explore Melocoton, a groundbreaking program logic for verifying interactions between OCaml and C components through OCaml's foreign function interface, mechanized in Coq using Iris.

• YouTube
• 1 hour 2 minutes
• Self-Paced
• Free Video

A Diagram Editor to Mechanize Categorical Proofs

Explore a prototype diagram editor for mechanizing categorical proofs, enhancing the process of creating diagrammatic proofs in Coq and UniMath.

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

Operational Algorithmic Game Semantics for Call-by-Push-Value Calculus

Explore operational algorithmic game semantics in a call-by-push-value calculus with state, examining trace models, automata, and full abstraction for programming language translations.

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

A Denotational Approach to Release/Acquire Concurrency - GALOP'24

Explore denotational semantics for Release/Acquire concurrency, focusing on trace semantics and game-like interpretations of program-environment interactions in shared-state languages.

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

Fair Omega-Regular Games

Explore two-player games with fairness constraints, focusing on fair α/β games. Learn about determinacy, polynomial reduction techniques, and symbolic algorithms for solving these complex game structures.

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

Fully Abstract Normal Form Bisimulation for Call-by-Value PCF

Explore a fully abstract normal form bisimulation for call-by-value PCF, combining applicative and environmental bisimulation with game semantics for program equivalence checking.

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

Operational Game Semantics for Generative Algebraic Effects and Handlers

Explore operational game semantics for generative algebraic effects and handlers in a typed call-by-value λ-calculus, focusing on dynamic allocation and first-class effect instances.

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

Game-Enriched Categories

Explore game-enriched categories as an enhanced approach to modeling programming languages, potentially offering greater flexibility in strategy definition.

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

Compositional Development of Certified System Software

Explore compositional development of certified system software, focusing on CertiKOS project's approach to specifying, programming, and compiling large-scale heterogeneous systems.

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

ImageEye: Batch Image Processing using Program Synthesis

Explore a novel synthesis-based approach for fine-grained batch image processing, combining neural networks and symbolic reasoning to automate object-specific edits within images.

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

Cakes That Bake Cakes: Dynamic Computation in CakeML

Explore CakeML compiler's new Eval primitive for runtime syntax evaluation, enabling dynamic execution and shared values between original and added code.

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

Leveraging Rust Types for Program Synthesis

Explore how Rust's type system enhances program synthesis, simplifying specifications and improving performance. Learn about Synthetic Ownership Logic and the RusSOL tool for automatic synthesis of correct Rust programs.

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

Parameterized Algebraic Protocols

Explore parameterized algebraic protocols for defining protocol templates and session types, enhancing expressiveness and modularity while enabling efficient type checking in linear time.

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

Proving and Disproving Equivalence of Functional Programming Assignments

Explore an automated approach for verifying programming assignments using equivalence checking, functional induction, and clustering algorithms. Learn how to prove correctness and provide counterexamples efficiently.

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

Probabilistic Programming with Stochastic Probabilities

Explore a novel approach to probabilistic programming languages using stochastic probability estimation, enabling unrestricted stochastic control flow and programmable inference with custom proposals.

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