COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Formalization of diagram chasing as a first-order logic in Coq

## Formalization of diagram chasing as a first-order logic in CoqAdd to your list(s) Download to your calendar using vCal - Dr Matthieu Piquerez (INRIA, Université de Nantes)
- Thursday 11 May 2023, 17:00-18:00
- Centre for Mathematical Sciences MR12, CMS.
If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki. Hybrid talk (please see abstract for link) Diagram chasing is at the heart of many powerful tools in mathematics. Unfortunately, their usage requires a lot of tedious and technical calculations. For instance, one has to check the commutativity of many diagrams. These technicalities are often not detailed in papers, and can be a source of mistakes. This motivates the development of a formalized library to do diagram chasing on computer. In particular, a large part of the above mentioned computations can be automatized. In this talk, after recalling the different notions, I will present the key points of such a library I am developing with Assia Mahboubi in Coq. In particular, I will explain that all the diagram chasing statements can be restated in a very simple language (in a first order logic), and I will state a formalized version of a often used duality meta-theorem. WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 379 992 884 209 Passcode: TYR8 Sh This talk is part of the Formalisation of mathematics with interactive theorem provers series. ## This talk is included in these lists:- Centre for Mathematical Sciences MR12, CMS
- All CMS events
- All Talks (aka the CURE list)
- CMS Events
- Cambridge talks
- DPMMS Lists
- DPMMS Pure Maths study groups
- DPMMS info aggregator
- DPMMS lists
- Department of Computer Science and Technology talks and seminars
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
Note that ex-directory lists are not shown. |
## Other listsUniversity Research Ethics Committee Events NormangeeStar Graduate Workshop in Economic and Social History## Other talksGateway TBA Ancient Bioinvasions: Can We Improve Evidentiary Standards for Species Introduction Research in Archaeology? Improved Prior Models for Physics-Driven Digital Twins Building your life-support system; a new paradigm for human placental development |