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)

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


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

(No recording available)


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

(No recording available)


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


Dagur Asgeirsson (University of Copenhagen): Condensed mathematics in Mathlib

Dagur Asgeirsson: Condensed mathematics in Mathlib


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


Mario Carneiro (Carnegie Mellon University): Impromptu chat about HB in Lean

Mario Carneiro: Impromptu chat about HB in Lean


Mirna Džamonja (IRIF (CNRS et Université Paris Cité) ): Calculating ordinal invariants - can you do better than a human ?

Mirna Džamonja: Calculating ordinal invariants - can you do better than a human ?


Jeremy Avigad (Carnegie Mellon University): A dry run

(No recording available)


Thomas Ammer (King's College London): Formalising and Verifying Algorithms for the Minimum Cost Flow Problem

(No recording available)


Maximilian Doré (Oxford University): Automating Reasoning in Cubical Type Theory

Maximilian Doré : Automating Reasoning in Cubical Type Theory


Valeria de Paiva (Topos Institute): Dialectica Categories for all

Valeria de Paiva: Dialectica Categories for all


Josef Urban (CIIRC - CTU): The Proofgold blockchain

Link to paper: https://doi.org/10.4230/OASIcs.FMBC.2022.4

See also: https://formalweb3.uibk.ac.at/pgbce/

Josef Urban: The Proofgold blockchain


Michael Kohlhase (FAU Erlangen-Nürnberg): Aspects of Mathematical Knowledge - The Tetrapod Model

Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model


Sebastian Ullrich (Lean FRO): Profiling Tools in Lean

Sebastian Ullrich: Profiling Tools in Lean


Paul-André Melliès (CNRS, Universite Paris Cite, INRIA): Fierce Discussion about ML and Proof Theory

(No recording available)


Peter Dybjer (Chalmers University of Technology): Inductive Definitions, Predicativity, and the Mahlo universe

Peter Dybjer: Inductive Definitions, Predicativity, and the Mahlo universe


Sina Hazratpour (Johns Hopkins University): Dependent Equalities in Lean4

(No recording available)

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


Evan Cavallo (Göteborgs universitet): Formalizing cubical interpretations of homotopy type theory

See https://arxiv.org/abs/2406.18497 and https://ecavallo.net/equivariant-cartesian/

Evan Cavallo: Formalizing cubical interpretations of homotopy type theory


Gisele D. Secco (California State University San Bernardino): From Computers to Diagrams and Back: The Four-Color Theorem and the Rise of a New Mathemartical Culture

(No recording available)


Shashank Pathak (The University of Manchester): GFLean - Autoformalisation for Lean via GF

Link to paper: https://arxiv.org/abs/2404.01234

Shashank Pathak: GFLean: Autoformalisation for Lean via GF


Rishikesh Vaishnav (École normale supérieure Paris-Saclay): Lean4Less - A Term-Patching Framework for Eliminating Defitional Equalities in Lean (Work in Progress)

Link to paper: https://lfmtp.github.io/lfmtp-page/workshops/2024/wip_1_vaishnav.pdf

Rishikesh Vaishnav: Lean4Less: A Term-Patching Framework for Eliminating Defitional Equalities in Lean


Mario Carneiro (Carnegie Mellon University): Lean4Lean - Formalizing the metatheory of Lean

Link to slides

Mario Carneiro: Lean4Lean: Formalizing the type theory of Lean


Kensho Tsurusaki (The University of Tokyo): Literate programming in Lean

I'll talk about implementing a system for "literate programming" in Lean.

Link to slides: https://drive.google.com/file/d/1GzrJ6liwSMrHTYZCLCyqo42FVCMa4v2X/view?usp=sharing

Kensho Tsurusaki: Literate programming in Lean


Mauricio Ayala-Rincón (Universidade de Brasília): Formalisation of nominal equations reasoning in PVS*

Nominal anti-unification (the library nasa/ pvslib/ nominal)

* Research supported by Brazilian agencies CAPES, CNPq, and FAPDF

Mauricio Ayala-Rincón: Formalisation of nominal equations reasoning in PVS


James Davenport (University of Bath): Branch Cuts and Formal Methods?

Link to updated slides: https://people.bath.ac.uk/masjhd/Slides/JHDatHIMBranchCuts.pdf

James Davenport: Branch Cuts and Formal Methods?


James Mckinna (Heriot-Watt University): Reflections on a career with/in type theory for formalised computer science/math

(No recording available)


Marco Maggesi (Università di Firenze): Mechanising Gödel–Löb Provability Logic in HOL Light

Link to paper: https://link.springer.com/article/10.1007/s10817-023-09677-z

Marco Maggesi: Mechanising Gödel–Löb Provability Logic in HOL Light


Thaynara Arielly de Lima (Universidade Federal de Goiás): Algebraic Theorems in PVS

Thaynara Arielly de Lima: Algebraic Theorems in PVS


Alexei Lisitsa (University of Liverpool): Gauss Realisability conditions - from error correction to formalization

Links to further resources:

Alexei Lisitsa: Gauss Realisability conditions - from error correction to formalization


Yutaka Nagashima (Independent): Abduction Prover in Isabelle/HOL

See also: https://youtu.be/rXU-lJxP_GI

Yutaka Nagashima: Abduction Prover in Isabelle/HOL


Raheleh Jalali (Institute of Computer Science, Czech Academy of Sciences): On the Completeness of Interpolation Algorithms

Link to publications:

Raheleh Jalali: On the Completeness of Interpolation Algorithms


Hannah Leung (University of Illinois Urbana-Champaign): Formally Verifying Functional Correctness of a Path Oblivious RAM algorithm

(No recording available)


Marco Caminati (Lancaster University Leipzig): Challenges in formalising recent results in formal language theory

In a recent paper (https://arxiv.org/abs/2405.09396), I introduced a new proof of a recent result linking formal language theory and computational group theory, one goal being to make its formalisation more feasible. I will discuss the state of this.

Marco Caminati: Challenges in formalising recent results in formal language theory

Wird geladen