BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Formalization of diagram chasing in proof assistants
DTSTART:20240125T110000
DTEND:20240125T120000
DTSTAMP:20260916T124155Z
UID:7e8973bb3755cdf717caa76a19c2739fe48471f0de1ec21811575c3b
CATEGORIES:Conferences - Seminars
DESCRIPTION:Matthieu Piquerez\, Nantes Université\nDiagram chasing is a k
 ind of diagrammatic reasonning at the heart of many powerful tools in math
 ematics. Unfortunately\, their usage requires a lot of tedious and technic
 al calculations. This motivates the development of a formalized library to
  do diagram chasing on computer. On the other hand\, proof assistants are 
 not well suited a priori to perform diagrammatic reasonning easily. In thi
 s talk\, after recalling the different notions\, I will present the key po
 ints of such a library I am developing with Assia Mahboubi in Coq.\n\nSpea
 ker bio: Matthieu Piquerez is a postdoctoral researcher in computer scienc
 e and mathematics at Nantes Université\, France\, in the Gallinette team 
 (INRIA). He works on enabling the use of diagrammatic reasoning and other 
 mathematical tools such as the commutativity of diagrams\, diagram-chasing
  proofs\, and spectral sequences\, in formal proofs in the Coq proof assis
 tant. He also works on tropical Hodge theory. He earned his PhD in 2021 fr
 om the École polytechnique\, France\, and his Master’s in 2017 from the
  École normale supérieure (ENS) Paris\, France.
LOCATION:BC 329 https://plan.epfl.ch/?room==BC%20329
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR