ACM SIGPLAN Courses

Nominal Recursors as Epi-Recursors - POPL 2024

Explore nominal recursors in syntax with bindings, comparing expressiveness and viewing them as epi-recursors. Develop a framework for comparison and apply to nominal corecursors, validated with Isabelle/HOL.

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

Monotonicity and the Precision of Program Analysis

Explore the connection between program monotonicity and analysis precision. Learn how monotone behavior enables complete abstract interpretation for numeric invariant inference.

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

When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism

Explore a novel type inference approach for first-class polymorphism using multi-bounded polymorphism, advancing the state of the art in type inference for programming languages.

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

Polymorphic Type Inference for Dynamic Languages

Explore a novel type system combining polymorphism, intersection types, and subtyping for dynamic languages. Learn about type reconstruction algorithms and their applications in advanced programming.

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

A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability

Explore a universal, sound, and complete proof method for machine-verifiable linearizability proofs. Learn about its application to complex algorithms and verification using TLAPS.

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

Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures

Explore a novel approach to probabilistic program inference using Gaussian mixtures, offering improved accuracy and efficiency for complex models and distributions.

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

Calculational Design of Correctness and Incorrectness Transformational Program Logics by Abstract Interpretation

Explore transformational program logics for correctness and incorrectness, extending to handle termination and nontermination. Learn a calculational method for designing sound and complete formal proof systems.

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

Optimal Program Synthesis via Abstract Interpretation - POPL 2024

Explore a framework for optimal program synthesis using abstract interpretation, improving scalability with A* search and heuristics for numerical constant optimization in domain-specific languages.

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

Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis

Explore a novel program analysis method generating polynomial arithmetic summaries, applicable to general programs with nested loops and complex control flow.

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

Effectful Software Contracts - Design and Implementation

Explore a universal principle for effectful contract systems using effect handlers, empowering programmers to constrain effects in software components with theoretical and practical insights.

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

Efficient Matching of Regular Expressions with Lookaround Assertions

Explore efficient matching of regular expressions with lookaround assertions, including formal semantics, simplification properties, and a new O(m·n) algorithm using oracle-NFAs for improved performance.

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

A Core Calculus for Documents - Lambda: The Ultimate Document

Explore a formal foundation for document languages, examining the interaction between passive documents and active programs. Learn about a document calculus for implementing features and proving theorems.

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

Mechanizing Refinement Types

Explore the mechanization of refinement types, combining semantic subtyping and parametric polymorphism. Learn about λRF calculus, data propositions, and metatheory proofs in LiquidHaskell and Coq.

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

Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

Explore a novel refinement type system for algebraic effects and handlers, introducing answer refinement modification to track effect occurrences and order in program execution.

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

Pipelines and Beyond: Graph Types for ADTs with Futures

Explore a novel graph type system enabling arbitrary combinations of futures and recursive data types in parallel programming, enhancing pipelining and performance optimization techniques.

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