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.facetsofcomplexity.de
URL:http://www.facetsofcomplexity.de/monday/20210628-L-Allamigeon.html
END:VEVENT
END:VCALENDAR