Displayed Monoidal Categories for the Semantics of Linear Logic
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a 30-minute conference talk from CPP 2024 that delves into the formalization of categorical structures used to interpret linear logic. Learn about the development of displayed monoidal categories as a solution to scalability challenges in formalizing complex mathematical objects. Discover how these structures enable modular construction of complicated monoidal categories and their application in defining linear-non-linear categories. Gain insights into the formalization process using UniMath, a library of univalent mathematics based on the Coq proof assistant. Understand the practical implications of this work for creating usable libraries of formalized results on monoidal categories and their role in interpreting linear logic.
Syllabus
[CPP'24] Displayed Monoidal Categories for the Semantics of Linear Logic
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