Modular Denotational Semantics for Effects with Guarded Interaction Trees
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 21-minute conference talk from POPL 2024 that introduces guarded interaction trees, a framework for representing higher-order computations with higher-order effects in Coq. Delve into the presentation of a structure inspired by domain theory and interaction trees, along with an accompanying separation logic for reasoning. Learn how guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects through the demonstration of a PCF-like language interpretation. Discover the modular approach to combining and reasoning about different effects, illustrated through a proof of type soundness for cross-language interactions. Gain insights into the formalization of all results in Coq using the Iris logic over guarded type theory, with available and reusable artifacts for further exploration.
Syllabus
[POPL'24] Modular Denotational Semantics for Effects with Guarded Interaction Trees
Taught by
ACM SIGPLAN
Related Courses
Verifying the LLVMStrange Loop Conference via YouTube Beweisbar sichere Software
media.ccc.de via YouTube RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story
Rust via YouTube Building Measure Theory Using Hierarchy Builder
Hausdorff Center for Mathematics via YouTube Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube