Building Measure Theory Using Hierarchy Builder
Offered By: Hausdorff Center for Mathematics via YouTube
Course Description
Overview
Explore the Hierarchy Builder Domain Specific Language for Coq and its application in constructing measure theory and the Lebesgue measure concisely. Delve into a 40-minute conference talk by Cyril Cohen at the Hausdorff Center for Mathematics, which aims to provoke discussions relevant to porting HB to other proof assistants. Gain insights into the collaborative work with Reynald Aeldt, Pierre Roux, Kazuhiko Sakaguchi, and Enrico Tassi as they demonstrate the practical implementation of this powerful tool in mathematical proofs.
Syllabus
Cyril Cohen: Building Measure Theory using Hierarchy Builder
Taught by
Hausdorff Center for Mathematics
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 Using Formal Methods to Eliminate Exploitable Bugs - YOW! 2015
GOTO Conferences via YouTube From 100 to 1000+ Theorems - Advancements in Mathematical Proof Verification
Hausdorff Center for Mathematics via YouTube