Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp4.
|
|
|
| Architecture | Package Size | Installed Size | Files |
|---|---|---|---|
| alpha | 8,684.1 kB | 24409 kB | no current information |
| arm | 8,247.4 kB | 22768 kB | no current information |
| hppa | 7,140.3 kB | 19896 kB | no current information |
| i386 | 7,986.2 kB | 21868 kB | no current information |
| ia64 | 9,680.8 kB | 28460 kB | no current information |
| m68k | 6,972.2 kB | 19480 kB | no current information |
| mips | 7,063.1 kB | 20532 kB | no current information |
| mipsel | 7,058.7 kB | 20532 kB | no current information |
| powerpc | 7,034.0 kB | 19744 kB | no current information |
| s390 | 7,038.9 kB | 19804 kB | no current information |
| sparc | 7,063.4 kB | 19772 kB | no current information |