BEGIN:VCALENDAR
CALSCALE:GREGORIAN
PRODID:iCalendar-Ruby
VERSION:2.0
BEGIN:VEVENT
DESCRIPTION: In this talk\, I will present the project Coq-Polyhedra that a
 ims at formalizing the theory of polyhedra as well as polyhedral computatio
 ns in the proof assistant Coq.  I will explain how the intuitionistic natur
 e of the logic of a proof assistant like Coq requires to define basic prope
 rties of polyhedra in a quite different way than is usually done\, by relyi
 ng on a formal proof of the simplex method. I will also focus on the formal
 ization of the faces of polyhedra\, and present a mechanism which automatic
 ally introduces an appropriate representation of a polyhedron or a face\, d
 epending on the context of the proof. I will demonstrate the usability of t
 his approach by establishing some of the most important combinatorial prope
 rties of faces\, namely that they constitute a family of graded atomistic a
 nd coatomistic lattices closed under interval sublattices\, as well as Bali
 nski’s theorem on the d-connectedness of the graph of d-polytopes. Finally\
 , I will discuss recent progress on the formal computation of the graph of 
 a polytope directly within the proof assistant\, thanks to a certified algo
 rithm that checks a posteriori the output of Avis’ vertex enumeration libra
 ry lrslib.  Joint work with Quentin Canu\, Ricardo D. Katz and Pierre-Yves 
 Strub. 
DTSTAMP:20210621T154200
DTSTART:20210628T141500
CLASS:PUBLIC
LOCATION:online
SEQUENCE:0
SUMMARY:Xavier Allamigeon (Inria and Ecole Polytechnique): Formalizing the 
 theory of polyhedra in a proof assistant
UID:107919067@/www.mi.fu-berlin.de
URL:https://www.mi.fu-berlin.de/en/facetsofcomplexity/monday/20210628-L-All
 amigeon.html
END:VEVENT
END:VCALENDAR