ACM SIGPLAN Courses

Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform - Incorrectness'24

Explore unified compositional formal methods for program correctness and incorrectness reasoning, focusing on exact separation logic and the Gillian platform.

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

InducTeX: A MetaCoq Plugin for Typesetting Inductive Definitions

Explore InducTeX, a MetaCoq plugin for typesetting Coq inductive definitions as TeX inference rules, streamlining documentation and communication of formal developments.

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

Functorial Syntax for All - Representing and Reasoning About Binding Structures

Explore a Coq library for reasoning about variable binding in programming languages using functorial syntax, with insights from development and application across projects.

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

Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

Explore Melocoton, a groundbreaking program logic for verifying interactions between OCaml and C components through OCaml's foreign function interface, mechanized in Coq using Iris.

• YouTube
• 1 hour 2 minutes
• On-Demand
• Free Video

A Diagram Editor to Mechanize Categorical Proofs

Explore a prototype diagram editor for mechanizing categorical proofs, enhancing the process of creating diagrammatic proofs in Coq and UniMath.

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

Operational Algorithmic Game Semantics for Call-by-Push-Value Calculus

Explore operational algorithmic game semantics in a call-by-push-value calculus with state, examining trace models, automata, and full abstraction for programming language translations.

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

A Denotational Approach to Release/Acquire Concurrency - GALOP'24

Explore denotational semantics for Release/Acquire concurrency, focusing on trace semantics and game-like interpretations of program-environment interactions in shared-state languages.

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

Fair Omega-Regular Games

Explore two-player games with fairness constraints, focusing on fair α/β games. Learn about determinacy, polynomial reduction techniques, and symbolic algorithms for solving these complex game structures.

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

Fully Abstract Normal Form Bisimulation for Call-by-Value PCF

Explore a fully abstract normal form bisimulation for call-by-value PCF, combining applicative and environmental bisimulation with game semantics for program equivalence checking.

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

Operational Game Semantics for Generative Algebraic Effects and Handlers

Explore operational game semantics for generative algebraic effects and handlers in a typed call-by-value λ-calculus, focusing on dynamic allocation and first-class effect instances.

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

Game-Enriched Categories

Explore game-enriched categories as an enhanced approach to modeling programming languages, potentially offering greater flexibility in strategy definition.

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

Haskell Symposium 2024 - Session 3

Explore advanced Haskell concepts and applications in this comprehensive symposium, featuring expert presentations and cutting-edge research in functional programming.

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

Haskell Symposium 2024 - Session 3

Explore advanced Haskell concepts and applications in this comprehensive symposium, featuring expert presentations and cutting-edge research in functional programming.

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

On the Power of Temporal Prophecy

Explore temporal prophecy's power in liveness and termination proofs, including its application to non-primitive recursive functions like Ackermann's.

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

How to Read a PL-Security Paper

Explore techniques for understanding PL-security papers, including threat models, attacker concepts, and contributions to programming languages. Gain insights for PL generalists approaching security topics.

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