Program of Coq

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