Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

34 lines (29 sloc) 1.383 kB
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,
Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega)
Pierre Courtieu, Lemme (contrib/funind)
Loïc 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
The Coq development Team (march 2004)
Bruno Barras (INRIA)
Pierre Corbineau (Université Paris Sud)
Jean-Christophe Filliâtre (CNRS)
Hugo Herbelin (INRIA)
Pierre Letouzey (Université Paris Sud)
Claude Marché (Université Paris Sud-INRIA)
Christine Paulin (Université Paris Sud)
Clément Renard (INRIA)
Jump to Line
Something went wrong with that request. Please try again.