Program

14:00-16:00 Session 1: Workshop TetraPod

Location: Old Library

14:00	Michael Kohlhase Aspects of Mathematical Knowledge (abstract)
15:00	Natarajan Shankar Modularity in Mathematical Knowledge (abstract)

16:30-18:00 Session 2: Workshop TetraPod

Location: Old Library

09:00-11:00 Session 3: CICM 2023 - Invited keynote & paper presentation

16:30	Catherine Dubois Isomorphisms and Interoperability (abstract)
17:15	Florian Rabe Panel discussion on the Mathematical Software of the Future (abstract)

Tuesday, September 5th

View this program: with abstracts session overview talk overview

Chair:

Manfred Kerber

09:00	Lawrence Paulson Large-Scale Formal Proof for the Working Mathematician – Lessons Learnt from the ALEXANDRIA Project (abstract)
10:00	Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener and Natarajan Shankar CoProver: A Recommender System for Proof Construction (abstract) PRESENTER: Natarajan Shankar
10:30	John Hester, Briland Hitaj, Grant Passmore, Sam Owre, Natarajan Shankar and Eric Yeh An Augmented MetiTarski Dataset for Real Quantifier Elimination using Machine Learning (abstract) PRESENTER: Grant Passmore

11:30-13:00 Session 4: CICM 2023 - Paper presentation

Location: Old Library

Chair:

Angeliki Koutsoukou-Argyraki

11:30	Marco B. Caminati Isabelle Formalisation of Original Representation Theorems (abstract)
12:00	Fabian Huch and Yiannos Stathopoulos Formalization Quality in Isabelle (abstract) PRESENTER: Fabian Huch
12:30	Aabid Seeyal Abdul Kharim, T.V.H. Prathamesh, Shweta Rajiv and Rishi Vyas Formalizing Free Groups in Isabelle/HOL: The Nielsen- Schreier Theorem and the Conjugacy Problem (abstract) PRESENTER: T.V.H. Prathamesh

14:00-16:00 Session 5: CICM 2023 - Paper presentation

Location: Old Library

Chair:

Michael Kohlhase

14:00	Jeffrey Shallit Proving Results About OEIS Sequences with Walnut (abstract)
14:30	Mauricio Ayala-Rincón, Maribel Fernandez, Gabriel Ferreira Silva, Temur Kutsia and Daniele Nantes-Sobrinho Nominal AC-Matching (Best Paper) (abstract) PRESENTER: Daniele Nantes-Sobrinho
15:00	Simone Heisinger and Martina Seidl True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers (abstract) PRESENTER: Simone Heisinger
15:20	Adam Naumowicz Extending Numeric Automation for Number Theory Formalizations in Mizar (abstract)
15:40	Florian Rabe and Stephen Watt Extracting Theory Graphs from the Aldor Library (abstract) PRESENTER: Florian Rabe

16:30-17:00 Session 6: CICM 2023 - Paper presentation

Location: Old Library

Chair:

Florian Rabe

17:00-18:00 Session 7: CICM 2023 - Open session

16:30

Eric Wieser

Multiple-inheritance hazards in dependently-typed algebraic hierarchies (abstract)

The open session is an opportunity for people to show their system developments on their laptops. In this session, people could also present other things, such as preliminary work, research proposals, offers of collaboration ...

Chair:

Florian Rabe

09:00-11:00 Session 8: CICM 2023 - Invited keynote & paper presentation

Wednesday, September 6th

View this program: with abstracts session overview talk overview

Chair:

Catherine Dubois

09:00	Martina Seidl Never Trust Your Solver: Certification for SAT and QBF (abstract)
10:00	James Davenport Proving an Execution of an Algorithm Correct? (abstract)
10:30	Jan Jakubuv and Cezary Kaliszyk VizAR: Visualization of Automated Reasoning Proofs (abstract) PRESENTER: Jan Jakubuv

11:30-13:00 Session 9: CICM 2023 - Paper presentation

Location: Old Library

Chair:

Adam Naumowicz

11:30	Mohit Tekriwal, Andrew Appel, Ariel Kellison, David Bindel and Jean-Baptiste Jeannin Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method (abstract) PRESENTER: Mohit Tekriwal
12:00	Neeraj Gangwar and Nickvash Kani Highlighting Named Entities in Input for Auto-Formulation of Optimization Problems (abstract) PRESENTER: Neeraj Gangwar
12:30	Jesús Aransay, Laureano Lambán and Julio Rubio Evasiveness through Binary Decision Diagrams (abstract) PRESENTER: Jesús Aransay

14:00-16:00 Session 10A: Doctoral Symposium

Location: Old Library

Chair:

Lawrence Paulson

Location: Queen's building

14:00	Muhammad Usama Sardar Formal Specification and Verification of Attestation in Confidential Computing (abstract)
14:20	Mahsa Ansari and Michael Monagan Doctoral Program Proposal Computing GCDs of Multivariate Polynomials over Algebraic Number Fields Presented with Multiple Extensions (abstract) PRESENTER: Mahsa Ansari
14:40	Luka Vrečar Towards computer-assisted semantic markup of mathematical documents (abstract)
15:00	Arjun Badyal Physics Engines for Verification of Robotic Systems (abstract)
15:20	Marcel Schütz Theory Morphisms in Computer Supported Education (abstract)

14:00-16:00 Session 10B: Workshop MathUI - Paper presentation

Chair:

Katja Beric

Location: Upper Hall

14:00	Abhishek Chugh, Michael Kohlhase and Dennis Müller Presentation of Active Documents in ALeA (abstract) PRESENTER: Abhishek Chugh
14:30	Andrea Kohlhase and Michael Kohlhase More Interactions in ALeA – Towards New Added-Value Services based on Semantic Markup (abstract) PRESENTER: Andrea Kohlhase
15:00	Takeo Noda, Takahiro Nakahara and Masataka Kaneko The learning constructs of inquiry-based mathematics learning represented in the log data of manipulating dynamic content (abstract) PRESENTER: Masataka Kaneko
15:30	Takuya Kitamoto Framework for building an E-Learning system using existing teaching materials (abstract)

14:00-16:00 Session 10C: Workshop NatFoM - Invited talk & Paper presentation

Chair:

Dennis Mueller

Location: Lecture Theatre 1 - William Gates Building/Computer Laboratory, Department of Computer Science and Technology, University of Cambridge

14:00	Roussanka Loukanova Type Theories for Computational Grammar of Natural Language (Invited Talk) (abstract)
15:00	Peter Koepke Experiences with Natural Language Proof Checking (abstract)
15:30	Adrian De Lon Scaling a natural proof assistant step by step (abstract)

16:30-18:00 Session 11A: Workshop MathUI - Paper presentation

Chair:

Abhishek Chugh

Location: Upper Hall

16:30	Shotaro Suzuki, Masahiro Nagasaki and Kazuhisa Nakasho Classification and Dependency Visualization of the Articles of the Mizar Mathematical Library (abstract) PRESENTER: Shotaro Suzuki
17:00	Michal Hudeček Digitising Advanced Interactions with Base Ten Blocks on a Grid (abstract)

16:30-18:00 Session 11B: Workshop NatFoM - Paper presentation

Chair:

Dennis Mueller

Location: Lecture Theatre 1 - William Gates Building/Computer Laboratory, Department of Computer Science and Technology, University of Cambridge

16:30	Bernhard Schröder Building small worlds in mathematical texts by formal and informal means (abstract)
17:00	Peter Koepke, Mateusz Marcol and Patrick Schäfer Formalizing Sets, Numbers, and some "Wiedijk Theorems" in Naproche (abstract) PRESENTER: Peter Koepke
17:30	Adrian De Lon Naproche Demo (abstract)

18:00-19:00 Session 12: Business Meeting

Chair:

William Farmer

Location: Upper Hall

Thursday, September 7th

View this program: with abstracts session overview talk overview

09:00-11:00 Session 13: CICM 2023 - Invited keynote & paper presentation

Chair:

Manfred Kerber

Location: Upper Hall

09:00	Mateja Jamnik How can we make trustworthy AI? (abstract)
10:00	Jonas Bayer, Alexey Gonus, Christoph Benzmüller and Dana Scott Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation (abstract) PRESENTER: Alexey Gonus
10:30	Christopher Brown, Zoltán Kovács, Tomas Recio, Robert Vajda and M. Pilar Velez GeoGebra Discovery (system entry) (abstract) PRESENTER: Zoltán Kovács

11:30-13:00 Session 14: CICM 2023 - Paper presentation

Location: Old Library

Chair:

William Farmer

Location: Upper Hall

11:30	Marc Berges, Jonas Betzendahl, Abhishek Chugh, Michael Kohlhase, Dominic Lohr and Dennis Müller Learning Support Systems based on Mathematical Knowledge Management (abstract) PRESENTER: Michael Kohlhase
12:00	Robert Corless, David J. Jeffrey and Azar Shakoori Teaching Linear Algebra in a mechanized mathematical environment (abstract) PRESENTER: Robert Corless
12:30	Jan Frederik Schaefer and Michael Kohlhase Towards an Annotation Standard for STEM Documents: Datasets, Benchmarks, and Spotters (abstract) PRESENTER: Jan Frederik Schaefer

14:00-16:00 Session 15A: Workshop MathUI - Paper presentation

Location: Old Library

Chair:

Andrea Kohlhase

Location: Upper Hall

14:00	Lukas Panzer and Jan Frederik Schaefer AnnoTize: A Flexible Annotation Tool for Documents with Mathematical Formulae (abstract) PRESENTER: Jan Frederik Schaefer
14:30	Haruka Miyata, Ryutaro Matsumoto and Kazuhisa Nakasho VSCode Extension for the Web and Coding Assistance for the Mizar Language (abstract) PRESENTER: Haruka Miyata
15:00	Valeria de Paiva, Qiyue Gao, Pavel Kovalev and Larry Moss Extracting Mathematical Concepts with Large Language Models (abstract) PRESENTER: Valeria de Paiva

14:00-16:00 Session 15B: Workshops NatFoM & Libraries of Formal Proofs and Natural Mathematical Language - Invited talk & Paper presentation

Chair:

Angeliki Koutsoukou-Argyraki

Location: Lecture Theatre 1 - William Gates Building/Computer Laboratory, Department of Computer Science and Technology, University of Cambridge

14:00	William Farmer Little Theories: A Method for Organizing Mathematical Knowledge Illustrated Using Alonzo, a Practice-Oriented Version of Simple Type Theory (Invited Talk) (abstract)
15:00	Lucy Horowitz MathGloss: Linked Undergraduate Math Concepts (abstract)
15:30	Marcel Schütz Foundational libraries in Naproche (abstract)

16:30-17:00 Session 16A: Workshops NatFoM & Libraries of Formal Proofs and Natural Mathematical Language - Paper presentation

Chair:

Peter Koepke

Location: Lecture Theatre 1 - William Gates Building/Computer Laboratory, Department of Computer Science and Technology, University of Cambridge

16:30

David Berry

Categorical Proofs are Natural Proofs (abstract)

16:30-18:00 Session 16B: Workshop MathUI - Demonstrations

Location: Upper Hall

16:30	Michal Hudeček Levebee (abstract)
16:50	Shotaro Suzuki Grouped Dependency Visualization Graph of Mizar Articles (abstract)
17:10	Abhishek Chugh ALeA (abstract)
17:30	Jan Frederik Schaefer AnnoTize (abstract)

17:00-18:00 Session 17: Workshops NatFoM & Libraries of Formal Proofs and Natural Mathematical Language - Panel discussion

Location: Lecture Theatre 1 - William Gates Building/Computer Laboratory, Department of Computer Science and Technology, University of Cambridge

18:45-22:00 Drinks and Dinner

Location: Dining Hall

Friday, September 8th

View this program: with abstracts session overview talk overview

09:00-11:00 Session 18: CICM 2023 - Invited keynote & paper presentation

Chair:

Catherine Dubois

Location: Upper Hall

09:00	Frédéric Blanqui Progress on proof systems interoperability (abstract)
10:00	Florian Rabe and Franziska Weber Morphism Equality in Theory Graphs (abstract) PRESENTER: Franziska Weber
10:30	Henry Hammer, Nanako Noda and Christopher Stone ProofLang: the Language of arXiv Proofs (abstract) PRESENTER: Christopher Stone

11:30-13:00 Session 19: CICM 2023 - Open session

Location: Old Library

Chair:

Andrea Kohlhase

Location: Upper Hall

11:30	Lars Hellström A Catalogue of Mathematical Objects — micropublishing knowledge of examples (abstract)
12:00	Peter Koepke Naproche demonstration (abstract)