Building Measure Theory Using Hierarchy Builder

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.