|
![](images/spacer.gif) |
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. |
|
|