Отправляет email-рассылки с помощью сервиса Sendsay
  Все выпуски  

Система компьютерной алгебры GAP: Coq Workshop (Coq-2) at FLOC



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-Franc,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

В избранное