Friday, July 9th
Friday's program is also available with abstracts and side by side with other events.
09:00‑10:00 Session 1
Location: AT 2.14
| 09:00 | Sean Wilson, Jacques Fleuriot and Alan Smaill Inductive Proof Automation for Coq |
| 09:30 | Chung-Kil Hur Heq: A Coq library for Heterogeneous Equality |
11:00‑12:30 Session 2
Location: AT 2.14
| 11:00 | Jean-francois Monin Proof Trick: Small Inversions |
| 11:30 | anne mulhern Strengthening the inversion Tactic in Coq |
| 12:00 | Keiko Nakata and Tarmo Uustalu Mixed induction-coinduction at work for Coq |
| 12:30 | Paolo Herms Certification of a chain for deductive program verification |
14:00‑15:00 Session 3
Location: AT 2.14
| 14:00 | Hugo Herbelin to be anounced |
| 14:30 | Thomas Braibant and Damien Pous Rewriting Modulo Associativity and Commutativity |
15:30‑17:00 Session 4
Location: AT 2.14
| 15:30 | Bas Spitters and Eelis van der Weegen Developing the algebraic hierarchy with type classes in Coq |
| 16:00 | Vladimir Komendantsky, Alexander Konovalov and Steve Linton Experience of interfacing Coq+SSReflect and GAP |
| 16:30 | Yves Bertot and Assia Mahboubi Root isolation for one-variable polynomials |