Universität Bonn

Seminar Series


James Davenport: Proving an execution of an algorithm correct

Link to paper: https://doi.org/10.1007/978-3-031-42753-4_17

James Davenport: Proving an execution of an algorithm correct


Nicolas Thiéry (Université Paris-Saclay): Categories, axioms, constructions in SageMath: Modeling mathematics for fun and profit

Link to slides: https://zenodo.org/records/12079015

Nicolas Thiéry: Categories, axioms, constructions in SageMath: Modeling mathematics for fun and profit


Michail Karatarakis: Formalizing Deligne's theorem (Number theory)

(Recording has not been edited, yet)

Video not found


Andrea Kohlhase: Eye Tracking for Math

Link to slides

Andrea Kohlhase: Eye Tracking for Math


Reed Mullanix: Cubical Type Theory for the Low-Dimensional Mathematician

(Pending permission to publish the recording)

Video not found


Emily Riehl (Johns Hopkins University): Formalizing ∞-category theory in the Rzk proof assistant

Link to repository: https://emilyriehl.github.io/yoneda/CPP-2024/

Link to slides: https://emilyriehl.github.io/files/colloquium-yoneda-in-rzk.pdf

Emily Riehl: Formalizing ∞-category theory in the Rzk proof assistant


Tom de Jong (University of Nottingham): Formalization in HoTT: equivalences, 3-for-2 and definitional equality

https://fplunchnott.wordpress.com/2023/12/08/a-practical-technique-for-proving-that-a-map-is-an-equivalence/

Tom de Jong: Formalization in HoTT: equivalences, 3-for-2 and definitional equality


Claudio Sacerdoti Coen (Alma Mater Studiorum - Università di Bologna): Indexing and Retrieval in a heterogeneous Formal Library

Claudio Sacerdoti Coen: Indexing and Retrieval in a heterogeneous Formal Library


Chris Lam (University of Illinois, Urbana-Champaign): Adventures in Correct-by-Construction Proof Engineering

Link to paper: https://doi.org/10.1145/3586052

(Pending permission to publish the recording)

Video not found


Harshit Motwani (Hong Kong University of Science and Technology): Formal Verification and Synthesis of Polynomial Programs using Algebro-Geometry

Link to paper: https://doi.org/10.1145/3586052

(No recording available)


Juan Meleiro (Universidade de São Paulo): Theory-oriented mathematics

Juan Meleiro: Theory-oriented mathematics


Milly Maietti (University of Padova) and Pietro Sabelli (University of Padua): Peculiarities of the Minimalist Foundation for Formal Mathematics

Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics


Cipriano Cioffo (Università degli Studi di Padova): A categorical account of the setoid model

Cipriano Cioffo: A categorical account of the setoid model


Sina Hazratpour (Johns Hopkins): Report on Polynomial Functors Formalization

Link to repository: https://github.com/sinhp/Poly/

Sina Hazratpour: Report on Polynomial Functors Formalization


Valeria de Paiva (Topos Institute): AI tools for Better Math

Valeria de Paiva: AI tools for Better Math


Davide Trotta (National Research Council, ISTI-CNR): Doctrines for Formal Mathematics

Link to slides

Davide Trotta: Doctrines for Formal Mathematics


Sina Hazratpour (Johns Hopkins): Linear Algebra Game in Lean

Link to repository: https://github.com/hhu-adam/Robo/tree/main

Sina Hazratpour: Linear Algebra Game in Lean


Wird geladen