BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalization of diagram chasing as a first-order logic in Coq - D
 r Matthieu Piquerez (INRIA\, Université de Nantes)
DTSTART:20230511T160000Z
DTEND:20230511T170000Z
UID:TALK196738@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:Diagram chasing is at the heart of many powerful tools in math
 ematics. Unfortunately\, their usage requires a lot of tedious and technic
 al calculations. For instance\, one has to check the commutativity of many
  diagrams. These technicalities are often not detailed in papers\, and can
 \nbe 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.\n\nIn this talk\, af
 ter recalling the different notions\, I will present the key points of suc
 h 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 formali
 zed version of a often used duality meta-theorem.\n\nWATCH ONLINE HERE : h
 ttps://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meetin
 g ID: 379 992 884 209 Passcode: TYR8 Sh
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR