Skip to Content.
Sympa Menu

coq-club - [Coq-Club] [Cfp] Coq Workshop, Edinburgh, July 9, Program and call for participation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [Cfp] Coq Workshop, Edinburgh, July 9, Program and call for participation


chronological Thread 
  • From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
  • To: Coq Club <coq-club AT inria.fr>, types AT lists.chalmers.se, types-announce AT lists.seas.upenn.edu, gdr-im AT gdr-im.fr, alp-diffusion AT univ-lille1.fr
  • Subject: [Coq-Club] [Cfp] Coq Workshop, Edinburgh, July 9, Program and call for participation
  • Date: Thu, 13 May 2010 18:51:06 +0200

Dear Colleague,

Please consider attending the Federated Logic Conference (FLoC) and especially

  the Coq Workshop (Coq-2)
  Edinburgh, July 9th, 2010

The early registration deadline is May 17th.

   http://www.floc-conference.org
   http://coq.inria.fr/coq-workshop/2010

The Coq workshop will bring together Coq users, developers and contributors. It will be organized from submitted and refereed presentations and more informal presentations. Please register and come participate in the discussions, even if you do not wish to submit any talks.

The workshop organizers

PROGRAM FOR THE COQ WORKSHOP
============================

Inductive Proof Automation for Coq

 by Sean Wilson, Jacques Fleuriot and Alan Smaill

Heq: A Coq library for Heterogeneous Equality

 by Chung-Kil Hur

Proof Trick: small Inversions

 by Jean-François Monin

Strengthening the inversion Tactic in Coq

 by anne mulhern

Mixed induction-coinduction at work for Coq

 by Keiko Nakata and Tarmo Uustalu

Certification of a chain for deductive program verification

 by Paolo Herms

Invited talk (title to be announced later)

 by Hugo Herbelin

Rewriting Modulo Associativity and Commutativity

 by Thomas Braibant and Damien Pous

Developing the algebraic hierarchy with type classes in Coq

 by Bas Spitters, Eelis van der Weegen

Experience of interfacing Coq+SSReflect and GAP

 by Vladimir Komendantsky, Alexander Konovalov and Steve Linton

Root isolation for one-variable polynomials

 by Yves Bertot and Assia Mahboubi




Archive powered by MhonArc 2.6.16.

Top of Page