ACM SIGPLAN Courses

Octagons Revisited - Elegant Proofs and Simplified Algorithms

Explore simplified algorithms for Octagon domain closure, featuring elegant proofs, efficient computations, and improved abstract transformers for affine assignments in program analysis.

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

Reuse and Automated Integration of Recommenders for Modelling Languages

Explore a methodology for reusing and integrating recommenders in modeling tools, addressing language, tool, source, and item dimensions. Learn about IronMan plugin for automating integration.

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

Scaling Up Machine Learning Without Tears - Programming Languages' Role

Explore techniques for scaling machine learning workloads across accelerators, focusing on partitioning, parallelism, and programming language concepts to optimize performance and hardware utilization.

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

Hydroflow: A Compiler Target for Fast, Correct Distributed Programs

Explore Hydroflow, a Rust-based dataflow runtime enabling correct program transformations for distributed systems. Learn about refactoring, replication, and partitioning techniques for optimizing distributed programs.

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

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference

Explore innovative approaches to improve type error messages in constraint-based type inference systems, focusing on data flow and subtyping constraints to enhance programmer understanding.

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

Scaling Verification of Concurrent Programs with the Civl Verifier

Learn to verify complex concurrent programs using Civl's layered refinement approach. Master techniques for simplifying proofs, enhancing maintainability, and scaling verification of advanced concurrent systems.

• YouTube
• 3 hours 30 minutes
• Self-Paced
• Free Video

String Solving for Verification - TutorialFest at POPL 2024

Explore string solving techniques for software verification, focusing on theory, implementations, and applications in programming languages and security analysis.

• YouTube
• 3 hours 31 minutes
• Self-Paced
• Free Video

Automated Datastructure Verification Using Unfoldings and SMT Solving - Foundations and FO-Completeness

Explore automated datastructure verification techniques using unfoldings and SMT solving. Learn foundations, FO-completeness, and applications in program verification.

• YouTube
• 2 hours 57 minutes
• Self-Paced
• Free Video

Foundations of Type-Driven Probabilistic Modelling

Explore type-driven abstractions for probabilistic modelling, covering discrete probability and quasi-Borel spaces. Gain hands-on experience through accompanying exercises for self-study.

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

MetaCoq Tutorial - Meta-programming and Proving with MetaCoq

Explore MetaCoq library for Coq meta-programming, learn to develop plugins and tactics, and understand metatheory for verifying meta-programs. Hands-on exercises included.

• YouTube
• 3 hours 28 minutes
• Self-Paced
• Free Video

A Type System for Elixir

Explore progress in adding static and gradual typing to Elixir, including set-theoretic types, bug detection, and mixing typed/untyped code. Learn about potential benefits and future challenges.

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

Vehicle - A Specification Language for Neural Network Properties

Explore Vehicle, a functional DSL for specifying neural network properties. Learn to express, compile, and verify specifications across platforms, enhancing safety in ML-enhanced systems.

• YouTube
• 3 hours 6 minutes
• Self-Paced
• Free Video

Teaching and Learning Compilers Incrementally - Tutorial

Explore incremental compiler development techniques for effective teaching and learning, enhancing understanding of language implementation concepts.

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

A Functional EDSL for Mathematics Visualization That Compiles to JavaScript - Demo

Explore Sylvester, a functional DSL for creating interactive math visualizations using F# and JSXGraph, designed for accessibility and ease of use without requiring web development expertise.

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

Perfectly Imperfect: Music, Math and the Keyboard

Explore the mathematical foundations of Western classical music, from Pythagoras to modern microtonal experiments, examining harmony, tuning systems, and rhythmic innovations through keyboard demonstrations.

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