ACM SIGPLAN Courses

SSA as Freyd Categories - Categorical Semantics for Compiler Design

Explore the connection between Static Single Assignment (SSA) and Freyd categories, examining their graphical syntax and applications in compiler design and optimization.

• YouTube
• 18 minutes
• On-Demand
• Free Video

Taylor Expansion and Game Semantics - Exploring Isomorphisms in Lambda Calculus

Explore the isomorphism between Taylor expansion of λ-terms and pointer concurrent games interpretation, extending previous results on resource terms and game semantics.

• YouTube
• 18 minutes
• On-Demand
• Free Video

MELL Proof-Nets Without Boxes: Thirty Years Later

Explore a novel approach to encoding exponentials as fixed-point operators in MELL proof-nets, eliminating boxes and interpreting non-wellfounded proofs as infinite MALL sequences.

• YouTube
• 18 minutes
• On-Demand
• Free Video

Covering All the Bases: Type-Based Verification of Test Input Generators

Explore a novel type-based verification method for validating coverage in test input generators, enhancing property-based testing with underapproximate reasoning and refinement types.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation

Explore a novel approach to inductive program synthesis using iterative forward-backward abstract interpretation, enhancing search space pruning and improving synthesis efficiency.

• YouTube
• 17 minutes
• On-Demand
• Free Video

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

Explore a novel automata-based approach for analyzing quantum circuits, enabling efficient verification and bug detection in large-scale quantum systems using tree automata and algebraic representations.

• YouTube
• 18 minutes
• On-Demand
• Free Video

Automated Expected Value Analysis of Recursive Programs

Explore automated inference of expected result values in probabilistic programs with recursion, procedures, and local variables. Learn about term representation and first-order constraints for analysis automation.

• YouTube
• 17 minutes
• On-Demand
• Free Video

Obtaining Information Leakage Bounds via Approximate Model Counting

Explore a sound symbolic quantitative information flow analysis for bounding information leakage in programs using approximate model counting and symbolic execution.

• YouTube
• 14 minutes
• On-Demand
• Free Video

WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly

Explore a verified monadic interpreter for WebAssembly, its adoption as a fuzzing oracle, and its performance compared to other interpreters and oracles.

• YouTube
• 17 minutes
• On-Demand
• Free Video

Mosaic: An Interoperable Compiler for Tensor Algebra

Explore Mosaic, an innovative compiler for sparse tensor algebra that combines external function calls and code fusion, offering flexibility and performance gains in tensor computations.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Mostly Automated Proof Repair for Verified Libraries

Explore automated proof repair for higher-order imperative functions, combining dynamic program alignment, enumerative invariant synthesis, and proof-driven testing to maintain verified software efficiently.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Fair Operational Semantics - Theory for Expressing and Reasoning About Fairness Properties

Explore Fair Operational Semantics (FOS), a novel theory for expressing and reasoning about fairness properties in program verification, with applications in concurrent systems and weak memory models.

• YouTube
• 20 minutes
• On-Demand
• Free Video

Extensible Metatheory Mechanization via Family Polymorphism

Explore a novel language design for extensible metatheory mechanization in proof assistants, utilizing family polymorphism for reusable code and proofs. Discover implementation, type theory, and case studies.

• YouTube
• 19 minutes
• On-Demand
• Free Video

Taype: A Policy-Agnostic Language for Oblivious Computation

Explore Taype, a novel language for secure multiparty computation that decouples security policies from program logic. Learn about oblivious algebraic data types and tape semantics for flexible, policy-agnostic development.

• YouTube
• 20 minutes
• On-Demand
• Free Video

PureCake: A Verified Compiler for a Lazy Functional Language - PLDI 2023

Explore PureCake, a verified compiler for PureLang, a lazy functional language. Learn about its Haskell-like syntax, type system, and end-to-end correctness proofs using HOL4 theorem prover.

• YouTube
• 17 minutes
• On-Demand
• Free Video