66 citations · 468 across the 34 of their papers we have counts for
3 papers · 1 filter
Formalizing the Face Lattice of Polyhedra
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistan…
A formalization of convex polyhedra based on the simplex method
Xavier Allamigeon, Ricardo D. Katz
We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof o…
Formal Proofs for Nonlinear Optimization
Victor Magron, Xavier Allamigeon, Stéphane Gaubert +1
We present a formally verified global optimization framework. Given a semialgebraic or transcendental function and a compact semialgebraic domain , we use the nonlinear maxp…