ACM SIGPLAN Courses

Dafny as Verification-Aware Intermediate Language for Code Generation

Explore how formal methods can improve LLM code generation by using Dafny as an intermediate language to validate correctness before compiling to target languages.

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

Baking for Dafny: A CakeML Backend for Dafny

Explore the development of a CakeML backend for Dafny that aims to reduce the trusted computing base by translating Dafny programs to CakeML, a verified subset of Standard ML, with functional big-step semantics.

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

Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean

Explore a methodology for handling complex Dafny program verification using Lean's interactive theorem prover, extracting straight-line programs and embedding Dafny's semantics to overcome automation limitations.

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

DafnyBench: A Benchmark for Formal Software Verification

Discover DafnyBench, the largest benchmark for training and evaluating ML systems in formal software verification, testing LLMs' ability to generate annotations for Dafny verification across 750+ programs.

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

Implementing OCaml APIs in Coq

Discover a lightweight design pattern for implementing OCaml APIs in Coq that preserves types and behaviors while supporting exceptions and mutable state, demonstrated through practical examples.

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

Formal Verification of Quantum Stabilizer Code

Explore the formal verification of quantum error correction codes using Coq and stabilizer group formalism to potentially reduce verification complexity.

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

A Domain-Specific PPL for Reasoning about Reasoning - A Memo on Memo

Explore memo, a domain-specific probabilistic programming language designed for theory of mind modeling, offering specialized syntax and efficient inference through array programming for faster, more concise models.

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

Data-oriented Design for Differentiable, Probabilistic Programming

Explore data-oriented design techniques for reimplementing LazyPPL's lazy rose tree structure, focusing on memory optimization and specialized reverse-mode autodiff for probabilistic programming.

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

My Journey in Secure Compilation

Explore the challenges and solutions in secure compilation, focusing on protecting programs from adversarial code and restricting undefined behavior through compartmentalization techniques like SECOMP for C code.

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

Sandwood: Runtime Adaptable Probabilistic Programming for Java

Discover Sandwood, an open-source probabilistic programming language for Java that enables easier integration of Bayesian models with runtime-adaptable configurations targeting different hardware and execution models.

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

Data-Parallel Differentiation by Optic Composition

Discover a data-parallel algorithm for computing reverse derivatives through optic composition, offering logarithmic time complexity on PRAM machines and linear time on sequential machines.

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

Semantics of the Memo Probabilistic Programming Language

Explore the formalization of memo, a domain-specific probabilistic programming language designed for reasoning about reasoning, including its type system and denotational semantics.

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

State Space Model Programming in Turing.jl

Explore state space models with SSMProblems.jl and GeneralisedFilters.jl, two Julia packages offering a composable, scalable framework for time-series analysis with advanced inference techniques like Kalman and particle filtering.

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

Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs

Explore the connection between probabilistic sampling and fresh name generation in the $\nu$-calculus through an abstract machine semantics that enables reasoning about contextual equivalence without direct sampling.

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

NP-NUTS: A Nonparametric No-U-Turn Sampler

Discover a hybrid algorithm combining NUTS and NP-HMC for efficient Hamiltonian Monte Carlo inference with automatic trajectory length adjustment and sampling from parameter spaces of varying dimensions.

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