1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
|
The Coq proof assistant V7 and V8 includes software developed by the
Coq development team inside the LogiCal project, at INRIA, CNRS and
University Paris Sud.
Copyright 1999-2004 The Coq development team,
INRIA-CNRS, University Paris Sud, All rights reserved.
This product includes also software developed by
Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface,
parsing/search.ml)
Pierre Crgut, France Telecom R & D (contrib/omega and contrib/romega)
Pierre Courtieu, Lemme (contrib/funind)
Loc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier)
Claudio Sacerdoti Coen, HELM, University of Bologna, (contrib/xml)
Coq includes a tactic Jp based on JProver, a theorem prover for
first-order intuitionistic logic. Jprover was originally implemented
by Stephan Schmitt and then integrated into MetaPRL by Aleksey
Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL
and then integrated it into Coq.
The file CREDITS contains a list of past contributors
The credits section in Reference Manual introduction details
contributions.
The Coq development Team (march 2004)
Bruno Barras (INRIA)
Pierre Corbineau (Universit Paris Sud)
Jean-Christophe Fillitre (CNRS)
Hugo Herbelin (INRIA)
Pierre Letouzey (Universit Paris Sud)
Claude March (Universit Paris Sud-INRIA)
Christine Paulin (Universit Paris Sud)
Clment Renard (INRIA)
|