File: COPYRIGHT

package info (click to toggle)
coq 8.0pl2-2
  • links: PTS
  • area: main
  • in suites: sarge
  • size: 14,228 kB
  • ctags: 17,685
  • sloc: ml: 97,070; makefile: 1,255; sh: 738; lisp: 456; awk: 15
file content (34 lines) | stat: -rw-r--r-- 1,383 bytes parent folder | download | duplicates (3)
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 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
contributions.

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)