Friday 27 May 2016, 10:30: Tests and Proofs for Enumerative Combinatorics, Catherine Dubois (ENSIIE).

Joint work with Alain Giorgetti and Richard Genestier

In this talk we show how enumerative combinatorics can benefit from testing and formal verification. We formalize in Coq the combinatorial structures of permutations and maps, and a couple of related operations. Before formally proving soundness theorems about these operations, we first validate them, by using logic programming (Prolog) for bounded exhaustive testing and Coq/QuickChick for random testing. It is an ex- perimental study preparing a more ambitious project about formalization of combinatorial results assisted by verification tools, including a library of formally specified and verified exhaustive generation algorithms.