BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
rem provers
SUMMARY:Formalization of diagram chasing as a first-order
logic in Coq - Dr Matthieu Piquerez (INRIA\, Unive
rsitÃ© de Nantes)
DTSTART;TZID=Europe/London:20230511T170000
DTEND;TZID=Europe/London:20230511T180000
UID:TALK196738AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/196738
DESCRIPTION:Diagram chasing is at the heart of many powerful t
ools in mathematics. Unfortunately\, their usage r
equires a lot of tedious and technical calculation
s. For instance\, one has to check the commutativi
ty of many diagrams. These technicalities are ofte
n not detailed in papers\, and can\nbe a source of
mistakes. This motivates the development of a for
malized library to do diagram chasing on computer.
In particular\, a large part of the above mention
ed computations can be automatized.\n\nIn this tal
k\, after recalling the different notions\, I will
present the key points of such a library I am dev
eloping with Assia Mahboubi in Coq. In particular\
, I will explain that all the diagram chasing stat
ements can be restated in a very simple language (
in a first order logic)\, and I will state a forma
lized version of a often used duality meta-theorem
.\n\nWATCH ONLINE HERE : https://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
CONTACT:Angeliki Koutsoukou-Argyraki
END:VEVENT
END:VCALENDAR