ACM SIGPLAN Courses

Let's Take Esoteric Programming Languages Seriously

Explore how esoteric programming languages like INTERCAL and Piet can enhance programming skills and language design awareness through their unique constraints and features.

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

Binary Search - Think Positive

Discover program verification in Agda through binary search algorithms with a positive approach to formal methods and correctness proofs.

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

A Guided Tour Through Oxidized OCaml

Explore OxCaml extensions for performance-oriented OCaml programming, covering fearless concurrency, data layouts, and allocation control for safer, faster code.

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

Mechanised Proofs of Atom Exhaustion in Erlang

Explore formal verification techniques for detecting atom exhaustion vulnerabilities in Erlang using mechanised proofs and the Coq proof assistant.

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

OCaml Blockly - A Block-Based Programming Environment for Functional Programming

Discover a block-based programming environment for OCaml that ensures error-free code through built-in scoping and typing rules, demonstrated via Tokyo metro pathfinding examples.

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

Girard's Paradox as Structure Music

Explore how Girard's paradox transforms into electronic music through Soundproof, translating proof terms of dependently typed lambda calculus into sonic tree structures.

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

Lexical Effect Handlers - Fast by Design, Correct by Proof

Discover how Lexa achieves state-of-the-art performance with lexically scoped effect handlers through innovative compiler design and formally verified correctness techniques.

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

What You See Is What It Does - A Structural Pattern for Legible Software

Discover a structural pattern for creating legible, modular software using concepts and synchronizations to improve incrementality, integrity, and transparency in LLM-assisted development.

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

Join Points in Practice

Discover how join points revolutionized functional compiler optimization through 8 years of GHC implementation experience, featuring insights from Simon Peyton Jones on practical lessons learned.

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

How Much Is in a Square? Calculating Functional Programs with Squares

Explore geometric reasoning in functional programming through "magic squares" - commutative squares that unify logic, databases, and formal semantics into elegant visual proofs.

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

typedKanren - Statically Typed Relational Programming with Exhaustive Matching in Haskell

Discover typedKanren, a statically typed miniKanren dialect in Haskell featuring exhaustive matching, disequality constraints, and generic programming support.

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

A Clash Course in Solving Sudoku - Functional Pearl

Explore hardware design using Haskell by building an FPGA Sudoku solver, transforming software implementation to hardware while preserving functional programming benefits.

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

Weft - Enabling Tidal on the Web

Explore Weft, a web-based Haskell-like interpreter that brings TidalCycles live coding to browsers with type inference and enhanced error reporting for interactive music performance.

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

The Proof Must Go On - Formal Methods in the Theater of Secure Software Development

Explore how formal methods will quietly transform software development from testing-based to verification-driven, becoming invisible infrastructure for secure systems.

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

Daisy - An Exercise Environment for Learning Information Modeling

Discover Daisy, a block-based environment that teaches information modeling through a structured three-step process, helping novice programmers represent problem data effectively.

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