ACM SIGPLAN Courses

Diagrammatic Notations for Interactive Theorem Proving

Explore innovative approaches to enrich interactive theorem provers with visual aids, focusing on composable diagram templates for enhanced proof development and presentation.

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

Exploratory Study on Multi-User Program Synthesis - A Multi-Wizard Approach

Explore multi-user program synthesis through a design experiment, investigating collaborative potential and effectiveness in software engineering and related domains.

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

Applying Large Scale Diffing to Declarative Configuration Code for Production Safety

Explore large-scale diffing for declarative configuration code to enhance production safety, addressing unintended consequences and testing challenges in config changes.

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

Ansible Is Turing Complete

Explore Ansible's unexpected Turing completeness through core language features. Discover how this configuration management tool achieves computational universality without relying on external languages or plugins.

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

Comprehensive Infrastructure as Code Testing - Creed for Speed

Explore ProTI, an automated unit testing approach for Infrastructure as Code programs, enabling rapid prototyping and efficient bug detection in cloud resource configurations.

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

Hybrid Execution: Combining Ahead-of-Time and Just-in-Time Compilation

Explore a novel approach combining AOT and JIT compilation for improved program execution, enhancing warm-up performance while maintaining peak efficiency in virtual machines.

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

Revisiting Dynamic Dispatch for Modern Architectures

Explore an alternative dispatch mechanism for dynamic languages, addressing modern hardware concerns while maintaining performance comparable to fully typed programs.

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

Beehive SPIR-V Toolkit: A Composable and Functional API for Runtime SPIR-V Code Generation

Explore a Java framework for dynamic SPIR-V binary module generation, offering faster compilation and improved performance for heterogeneous hardware offloading in TornadoVM.

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

Strongly-Typed Multi-View Stack-Based Computations

Explore a Domain-Specific Language for stack-based computations, ensuring type correctness and supporting multiple views and mutually recursive functions of arbitrary arities.

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

StableKanren: Integrating Stable Model Semantics with MiniKanren

Explore stableKanren, an innovative miniKanren extension supporting normal logic programming with stable model semantics. Learn about dynamic search streams and non-monotonic reasoning in functional programming.

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

Comprehending Queries over Finite Maps - Language-Integrated Query Techniques

Explore language-integrated query techniques, focusing on embedding database queries in programming languages and normalizing them for DBMS translation, including grouping and aggregation.

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

Additive Cellular Automata Graded-Monadically

Explore cellular automata through graded comonadic and monadic perspectives, focusing on additive variants and their computational implications.

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

Termination in Concurrency, Revisited - PPDP23

Explore termination in concurrent programming, comparing type systems for mobile processes and examining session types, weight-based systems, and Curry-Howard correspondence.

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

Data-Dependent Confidentiality in DCR Graphs

Explore DCRSec, a confidentiality-aware process language using data-dependent security levels and information flow monitoring to prevent policy violations in declarative processes.

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

Coq: The World's Best Macro Assembler? - 10-Year Most Influential Paper Talk

Explore a Coq formalization of x86 architecture, emphasizing brevity through dependent types and notation. Learn about concrete modeling of bits and bytes, and assembly code syntax within Coq.

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