Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

SSA as Freyd Categories - Categorical Semantics for Compiler Design

ACM SIGPLAN via YouTube

Overview

Explore the fundamental connection between Static Single Assignment (SSA) and Freyd categories in this insightful conference talk from GALOP'24. Delve into the mathematical foundations of modern compiler design as Jad Elkhaleq Ghalayini presents a novel perspective on SSA's wide applicability across various domains. Discover how SSA without control-flow relates to Freyd categories and learn about its graphical representation using string diagrams. Examine the correspondence between SSA with terminating control-flow and distributive Freyd categories, as well as the relationship between general control-flow SSA and Elgot structures. Gain insights into the type-theoretic presentation of isotope-SSA and its categorical semantics, understanding how various optimizations align with this framework. Explore models exhibiting interesting features, including a simple model of TSO-style weak memory. If time permits, learn about the generalization of the IR to support substructural types and impure substitutions, with potential applications in separation logic, quantum computing, and nondeterminism.

Syllabus

[GALOP'24] SSA is Freyd Categories

Taught by

ACM SIGPLAN

Reviews

Start your review of SSA as Freyd Categories - Categorical Semantics for Compiler Design

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.