|
|
 |
|
Vendredi 29 Novembre
| Heure: |
10:00 - 12:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Présentation de l2coq : une bibliothèque pour des preuves linéaires en Coq |
| Description: |
Micaela Mayero Dans cette séance je présenterai l2coq, développé par O. Laurent et D.
Pous. Il s'agit d'un "sous-ensemble de Coq" (sous la forme d'une
bibliothèque "restrictive") permettant de faire des preuves de
propriétés linéaires (ILL, ELL, LLL, SLL). Olivier en avait fait une
présentation le jour de la soutenance d'HDR de Virgile. En 1 an, l2coq a
continué d'évoluer. Je vous propose de revenir sur les bases de l2coq en
vous montrant également le code et j'expliquerai pourquoi j'ai mis
quelques mots entre guillemet dans les phrases précédentes. Pour cela,
je ferai des rappels (ou pas pour certains) de la théorie de Coq en me
basant sur l'exposé précédent de Christophe, la partie théorie des
types. Vers la fin ou en cours d'exposé, je vous ferai une démo, durant
laquelle nous pourrons tenter ensemble de faire des preuves formelles de
propriétés linéaires (ILL dans un premier temps). |
| Heure: |
12:00 - 13:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Vector space decomposition for linear programming |
| Description: |
Jacques Desrosiers This presentation describes a vector space decomposition algorithm for
a linear program with bounded variables. Given a current feasible
solution, the exchange mechanism towards the next one is split into
independent parts based on two orthogonal vector subspaces, that is,
the master and the subproblem ones. The subproblem generates
directions (rays) compatible with the vector subspace of the master
problem. Indeed the subproblem partially satisfies the exchange
mechanism that is completed at the master level. Special cases of this
generic vector space decomposition algorithm are, amongst others, the
Primal Simplex, the Improved Primal Simplex yielding non-degenerate
pivots only, the Dynamic Constraints Aggregation method for the set
partitioning problem, and the strongly polynomial Minimum Mean
Cycle-Cancelling algorithm for the capacitated network flow problem. |
|
|
