May
June
| Mon 3, 15:00 |
Chris Lam: Adventures in Correct-by-Construction Proof Engineering |
| Tue 4, 15:00 |
Harshit Motwani: Formal Verification and Synthesis of Polynomial Programs using Algebro-Geometry |
| Wed 5, 15:00 |
|
| Thu 6, 15:00 |
Milly Maietti and Pietro Sabelli: Peculiarities of the Minimalist Foundation for Formal Mathematics |
| Fri 7, 15:00 |
|
| Mon 10, 15:00 |
Sina Hazratpour: Report on Polynomial Functors Formalization |
| Tue 11, 15:00 |
|
| Wed 12, 15:00 |
|
| Thu 13, 15:00 |
|
| Fri 14, 15:00 |
|
| Mon 24, 15:00 | |
| Tue 25, 15:00 |
Mirna Džamonja: Calculating ordinal invariants - can you do better than a human? |
| Wed 26, 15:00 |
|
| Thu 27, 15:00 |
Thomas Ammer: Formalising and Verifying Algorithms for the Minimum Cost Flow Problem |
| Fri 28, 15:00 |
Maximilian Doré: Automating Reasoning in Cubical Type Theory |
July
| Mon 1, 15:00 | |
| Tue 2, 15:00 |
|
| Wed 3, 15:00 |
Michael Kohlhase: Aspects of Mathematical Knowledge - The Tetrapod Model |
| Thu 4, 15:00 |
|
| Fri 5, 15:00 |
Paul Andre Mellies: Fierce Discussion about ML and Proof Theory |
| Mon 15, 15:00 |
Peter Dybjer: Inductive Definitions, Predicativity, and the Mahlo universe |
| Tue 16, 15:00 |
|
| Thu 18, 15:00 |
Evan Cavallo: Formalizing cubical interpretations of homotopy type theory |
| Fri 19, 15:00 |
|
| Mon 22, 15:00 |
|
| Tue 23, 15:00 |
|
| Wed 24, 15:00 |
Mario Carneiro: Lean4Lean - Formalizing the metatheory of Lean |
| Thu 25, 15:00 |
August
| Mon 5, 15:00 | |
| Tue 6, 15:00 | |
| Wed 7, 15:00 |
James Mckinna: Reflections on a career with/in type theory for formalised computer science/math |
| Thu 8, 15:00 |
Marco Maggesi: Mechanising Gödel–Löb Provability Logic in HOL Light |
| Fri 9, 15:00 | |
| Mon 12, 15:00 |
Alexei Lisitsa: Gauss Realisability conditions - from error correction to formalization |
| Tue 13, 15:00 | |
| Wed 14, 15:00 |
Raheleh Jalali: On the Completeness of Interpolation Algorithms |
| Wed 14, 15:30 |
Hannah Leung: Formally Verifying Functional Correctness of a Path Oblivious RAM algorithm |
| Thu 15, 15:00 |
Marco Caminati: Challenges in formalising recent results in formal language theory |
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
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
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
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
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