1176:
1162:
76:
2522:
2512:
2502:
2492:
191:
2372:
828:, which was completed in 2002. Their work led to the development of the SSReflect ("Small Scale Reflection") package, which was a significant extension to Coq. Despite its name, most of the features added to Coq by SSReflect are general-purpose features and are not limited to the computational reflection style of proof. These features include:
310:
was also part of the project. The development of Coq was initiated by GĂ©rard Huet and
Thierry Coquand, and more than 40 people, mainly researchers, have contributed features to the core system since its inception. The implementation team has successively been coordinated by GĂ©rard Huet, Christine
924:
written in the built-in language Ltac or in OCaml. These tactics automate the construction of proofs, carrying out trivial or obvious steps in proofs. Several tactics implement decision procedures for various theories. For example, the "ring" tactic decides the theory of equality modulo
350:
was started and the name was changed from CoC to Coq in an indirect reference to
Coquand, who developed the Calculus of Constructions along with GĂ©rard Huet and contributed to the Calculus of Inductive Constructions with Christine Paulin-Mohring.
1142:("congruence"), propositional logic ("tauto"), quantifier-free linear integer arithmetic ("lia"), and linear rational/real arithmetic ("lra"). Further decision procedures have been developed as libraries, including one for
263:
in French meaning rooster). On
October 11th, 2023, the development team announced that Coq will be renamed "The Rocq Prover" in the coming months, and has started updating the code base, website and associated tools.
362:
property, implying that they always terminate. This is a distinctive property of the language, since infinite loops (non-terminating programs) are common in other programming languages, and is one way to
1799:. Interactive Theorem Proving: First International Conference, ITP 2010 Edinburgh, UK, July 11-14, 2010, Proceedings. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. pp. 163–178.
205:
first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the
370:
As an example, consider a proof of a lemma that taking the successor of a natural number flips its parity. The fold-unfold tactic introduced by Danvy is used to help keep the proof simple.
259:
The name "Coq" is a wordplay on the name of
Thierry Coquand, Calculus of Constructions or "CoC" and follows the French computer science tradition of naming software after animals (
817:
287:
2022:
907:: The value of the 5-state winning busy beaver was discovered by Heiner Marxen and Jürgen Buntrock in 1989, but only proved to be the winning fifth busy beaver — stylized as
27:
342:
and stems from a French tradition of naming research development tools after animals. Up until 1991, Coquand was implementing a language called the
2592:
2582:
303:
1842:
Theorem
Proving in Higher Order Logics: 17th International Conference, TPHOLS 2004, Park City, Utah, USA, September 14–17, 2004, Proceedings
1673:
Grégoire, Benjamin; Mahboubi, Assia (2005). "Proving
Equalities in a Commutative Ring Done Right in Coq". In Hurd, Joe; Melham, Tom (eds.).
1263:
1531:
Conchon, Sylvain; Filliâtre, Jean-Christophe (2007). "A persistent union-find data structure". In Russo, Claudio V.; Dreyer, Derek (eds.).
1453:
1295:
359:
2572:
2516:
1556:
2029:
2506:
1676:
Theorem
Proving in Higher Order Logics: 18th International Conference, TPHOLs 2005, Oxford, UK, August 22–25, 2005, Proceedings
1857:
1812:
1753:
1738:
Types for Proofs and
Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18–21, 2006, Revised Selected Papers
1692:
307:
2557:
1406:
1181:
2056:
347:
237:
214:
252:, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, and Pierre Castéran with the 2013
2562:
1581:
1305:
166:
149:
2001:
1194:
892:
276:
2334:
2187:
2095:
364:
194:
An interactive proof session in CoqIDE, showing the proof script on the left and the proof state on the right.
2577:
2552:
2107:
2129:
1996:
1913:– a library to process Coq snippets embedded in documents, showing goals and messages for each Coq sentence
876:
99:
67:
2227:
2463:
2322:
2173:
2084:
1199:
1630:
Kaiser, Jan-Oliver; Ziliani, Beta; Krebbers, Robbert; RĂ©gis-Gianas, Yann; Dreyer, Derek (2018-07-30).
1511:
2547:
2289:
2203:
2152:
2089:
2038:
1844:. Lecture Notes in Computer Science. Vol. 3223. Berlin, Heidelberg: Springer. pp. 225–240.
1189:
898:
343:
253:
218:
2453:
1740:. Lecture Notes in Computer Science. Vol. 4502. Berlin, Heidelberg: Springer. pp. 48–62.
1204:
886:
316:
299:
249:
222:
75:
1769:
843:
Implicit arguments for functions applied to zero arguments, which is useful when programming with
2567:
2526:
2193:
2015:
1837:
1794:
295:
1733:
2587:
2328:
1924:– widely used library of mathematical structures, part of which is the SSReflect proof language
346:
and it was simply called CoC at this time. In 1991, a new implementation based on the extended
291:
2380:
2308:
1708:
844:
2491:
2485:
1560:
1466:
938:
934:
821:
230:
210:
941:
rewriting. For example, the following proof establishes a complex equality in the ring of
8:
2061:
1407:"Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant"
1392:
320:
2394:
1969:
1953:
1863:
1818:
1770:"Micromega: solvers for arithmetic goals over ordered rings — Coq 8.18.0 documentation"
1674:
1167:
926:
825:
805:
280:
206:
1445:
2448:
1853:
1808:
1749:
1688:
1658:
1426:
1388:
1301:
1161:
1867:
1793:
Braibant, Thomas; Pous, Damien (2010). Kaufmann, Matt; Paulson, Lawrence C. (eds.).
1679:. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer. pp. 98–113.
1375:
1217:
2214:
1845:
1822:
1800:
1741:
1680:
1653:
1643:
1538:
1493:
1418:
833:
801:
161:
129:
1497:
1282:
1224:
2443:
2294:
1849:
1804:
1462:
339:
311:
Paulin-Mohring, Hugo
Herbelin, and Matthieu Sozeau. Coq is mainly implemented in
241:
202:
154:
1910:
1745:
1297:
Interactive
Theorem Proving: 9th International Conference, ITP 2018, Held as ...
358:" in Latin, Spanish, Italian and Catalan). Programs written in Gallina have the
2458:
2400:
1534:
Proceedings of the ACM Workshop on ML, 2007, Freiburg, Germany, October 5, 2007
1238:
1143:
837:
273:
134:
2406:
1422:
920:
In addition to constructing Gallina terms explicitly, Coq supports the use of
245:
2541:
2136:
1430:
1354:
1907:– allows Coq to run in a web browser, with no need to install extra software
1542:
2424:
2418:
2412:
2280:
2164:
1992:
1139:
2496:
1328:
2141:
2120:
1965:
1921:
1481:
904:
329:
283:
1975:
863:
SSReflect 1.11 is freely available, dual-licensed under the open source
1988:
1684:
226:
190:
34:
2314:
2256:
809:
1840:. In Slind, Konrad; Bunker, Annette; Gopalakrishnan, Ganesh (eds.).
1648:
1631:
1532:
2430:
2221:
2047:
1941:
1147:
930:
882:
864:
1932:
1916:
2360:
2274:
2244:
2198:
2007:
1959:
1629:
942:
813:
355:
335:
1978:– a tutorial on SSReflect by Georges Gonthier and Assia Mahboubi
1937:
2340:
2268:
2232:
2101:
1898:
1709:"The ring and field tactic families — Coq 8.11.1 documentation"
1516:
1333:
1268:
1734:"Fast Reflexive Arithmetic Tactics the Linear Case and Beyond"
832:
Additional convenient notations for irrefutable and refutable
2371:
2346:
2262:
2146:
2078:
1904:
1582:"[July 2nd 2024] We have proved "BB(5) = 47,176,870""
1387:
Adam Chlipala. "Certified Programming with Dependent Types":
1374:
Adam Chlipala. "Certified Programming with Dependent Types":
796:
312:
122:
105:
2250:
2238:
2070:
1606:
26:
286:. The development of Coq has been supported since 1984 by
1894:
1355:"Introduction to the Calculus of Inductive Constructions"
901:: formal proof using Coq was completed in September 2012.
1927:
1138:
Built-in decision procedures are also available for the
272:
When viewed as a programming language, Coq implements a
177:
1557:"Feit-Thompson theorem has been totally checked in Coq"
1537:. Association for Computing Machinery. pp. 37–46.
354:
Coq provides a specification language called Gallina ("
1886:
889:
which is largely programmed and proven correct in Coq.
867:
or CeCILL-2.0 license, and compatible with Coq 8.11.
1796:
An Efficient Coq Tactic for Deciding Kleene Algebras
1632:"Mtac2: typed tactics for backward reasoning in Coq"
1157:
279:; when viewed as a logical system, it implements a
1956:– a book on Coq by Yves Bertot and Pierre Castéran
1736:. In Altenkirch, Thorsten; McBride, Conor (eds.).
1482:"An introduction to small scale reflection in Coq"
895:: correctness proof in Coq was published in 2007.
2539:
1976:An introduction to small scale reflection in Coq
1672:
1559:. Msr-inria.inria.fr. 2012-09-20. Archived from
1530:
1479:
877:Proof assistant § Notable formalized proofs
225:but includes automatic theorem proving tactics (
1636:Proceedings of the ACM on Programming Languages
1294:Avigad, Jeremy; Mahboubi, Assia (3 July 2018).
885:: an optimizing compiler for almost all of the
1962:– online and printed textbook by Adam Chlipala
1293:
319:. The core system can be extended by way of a
2023:
1792:
1512:"The Mathematical Components Library 1.11.0"
1454:Notices of the American Mathematical Society
327:
1480:Gonthier, Georges; Mahboubi, Assia (2010).
2030:
2016:
1960:Certified Programming with Dependent Types
1838:"A Decision Procedure for Geometry in Coq"
797:Four color theorem and SSReflect extension
74:
25:
1657:
1647:
2388:
1443:
189:
2593:Extensible syntax programming languages
1989:Introduction to the Coq Proof Assistant
1928:Constructive Coq Repository at Nijmegen
1835:
2540:
1731:
2583:Programming languages created in 1984
2011:
1446:"Formal Proof—The Four-Color Theorem"
1404:
870:
213:. Coq works within the theory of the
1182:Free and open-source software portal
348:Calculus of Inductive Constructions
238:Association for Computing Machinery
215:calculus of inductive constructions
13:
2037:
1437:
1239:"Alternative names · coq/coq Wiki"
915:
856:tactic with more powerful matching
14:
2604:
2573:Free software programmed in OCaml
1878:
1411:Journal of Functional Programming
2521:
2520:
2511:
2510:
2501:
2500:
2490:
2370:
1174:
1160:
1922:Mathematical Components library
1905:JsCoq Interactive Online System
1829:
1786:
1762:
1725:
1701:
1666:
1623:
1599:
1574:
1549:
1524:
1504:
1486:Journal of Formalized Reasoning
1473:
1398:
911:— in 2024 using a proof in Coq.
791:
277:functional programming language
2335:Logic for Computable Functions
1381:
1368:
1347:
1321:
1287:
1276:
1256:
1231:
1:
1210:
1997:Institute for Advanced Study
1850:10.1007/978-3-540-30142-4_17
1805:10.1007/978-3-642-14052-5_13
1329:"Frequently Asked Questions"
840:with one or two constructors
290:, now in collaboration with
7:
2558:Dependently typed languages
1746:10.1007/978-3-540-74464-1_4
1607:"The Busy Beaver Challenge"
1498:10.6092/ISSN.1972-5787/1979
1283:A short introduction to Coq
1195:Curry–Howard correspondence
1153:
945:in just one line of proof:
893:Disjoint-set data structure
849:Concise anonymous arguments
267:
10:
2609:
1444:Gonthier, Georges (2008).
1200:Intuitionistic type theory
874:
203:interactive theorem prover
2563:Educational math software
2472:
2379:
2368:
2288:
2213:
2162:
2153:Standard ML of New Jersey
2119:
2069:
2055:
2046:
1732:Besson, Frédéric (2007).
1659:21.11116/0000-0003-2E8E-B
1586:The Busy Beaver Challenge
1423:10.1017/S0956796822000107
1190:Calculus of constructions
365:avoid the halting problem
344:Calculus of Constructions
254:ACM Software System Award
219:calculus of constructions
172:
160:
148:
140:
128:
118:
98:
94:
66:
62:
43:
33:
24:
2454:Christine Paulin-Mohring
1901:, source code repository
1836:Narboux, Julien (2004).
1393:"Library InductiveTypes"
1205:List of proof assistants
1146:and another for certain
947:
654:successor_flips_evenness
372:
300:Paris Diderot University
250:Christine Paulin-Mohring
223:automated theorem prover
39:The Coq development team
2527:Category:Software:OCaml
1543:10.1145/1292535.1292541
1405:Danvy, Olivier (2022).
816:and Benjamin Werner of
296:University of Paris-Sud
887:C programming language
859:Support for reflection
845:higher-order functions
328:
217:, a derivative of the
195:
49:; 35 years ago
2517:Category:Family:OCaml
1968:– online textbook by
899:Feit–Thompson theorem
820:used Coq to create a
729:fold_unfold_is_even_S
570:fold_unfold_is_even_S
525:fold_unfold_is_even_0
193:
81:; 23 days ago
2578:Functional languages
2553:Free theorem provers
2486:Open-source software
1966:Software Foundations
1642:(ICFP): 78:1–78:31.
1389:"Library GeneralRec"
1225:"Release Coq 8.20.0"
211:formal specification
2002:Coq Video tutorials
1991:– video lecture by
1376:"Library Universes"
1227:. 3 September 2024.
292:École Polytechnique
21:
2507:Category:Family:ML
2395:Lennart Augustsson
1970:Benjamin C. Pierce
1685:10.1007/11541868_7
1168:Mathematics portal
871:Other applications
826:four color theorem
806:Microsoft Research
636:fold_unfold_tactic
552:fold_unfold_tactic
378:fold_unfold_tactic
360:weak normalization
207:constructive proof
196:
79:/ 3 September 2024
19:
2535:
2534:
2449:Steven G. Johnson
2439:
2438:
2356:
2355:
2215:Programming tools
2183:
2182:
1859:978-3-540-30142-4
1814:978-3-642-14052-5
1755:978-3-540-74464-1
1694:978-3-540-31820-0
1461:(11): 1382–1393.
1264:"Coq roadmap 069"
274:dependently typed
188:
187:
2600:
2548:Proof assistants
2524:
2523:
2514:
2513:
2504:
2503:
2494:
2386:
2385:
2374:
2295:proof assistants
2067:
2066:
2053:
2052:
2032:
2025:
2018:
2009:
2008:
1890:
1889:
1887:Official website
1872:
1871:
1833:
1827:
1826:
1790:
1784:
1783:
1781:
1780:
1766:
1760:
1759:
1729:
1723:
1722:
1720:
1719:
1705:
1699:
1698:
1670:
1664:
1663:
1661:
1651:
1627:
1621:
1620:
1618:
1617:
1603:
1597:
1596:
1594:
1593:
1578:
1572:
1571:
1569:
1568:
1553:
1547:
1546:
1528:
1522:
1521:
1508:
1502:
1501:
1477:
1471:
1470:
1450:
1441:
1435:
1434:
1402:
1396:
1385:
1379:
1372:
1366:
1365:
1363:
1361:
1351:
1345:
1344:
1342:
1341:
1325:
1319:
1318:
1316:
1314:
1291:
1285:
1280:
1274:
1273:
1260:
1254:
1253:
1251:
1249:
1235:
1229:
1228:
1221:
1184:
1179:
1178:
1177:
1170:
1165:
1164:
1134:
1131:
1128:
1125:
1122:
1119:
1116:
1113:
1110:
1107:
1104:
1101:
1098:
1095:
1092:
1089:
1086:
1083:
1080:
1077:
1074:
1071:
1068:
1065:
1062:
1059:
1056:
1053:
1050:
1047:
1044:
1041:
1038:
1035:
1032:
1029:
1026:
1023:
1020:
1017:
1014:
1011:
1008:
1005:
1002:
999:
996:
993:
990:
987:
984:
981:
978:
975:
972:
969:
966:
963:
960:
957:
954:
951:
855:
834:pattern matching
822:surveyable proof
802:Georges Gonthier
787:
784:
781:
778:
775:
772:
769:
766:
763:
760:
757:
754:
751:
748:
745:
742:
739:
736:
733:
730:
727:
724:
721:
718:
715:
712:
709:
706:
703:
700:
697:
694:
691:
688:
685:
682:
679:
676:
673:
670:
667:
664:
661:
658:
655:
652:
649:
646:
643:
640:
637:
634:
631:
628:
625:
622:
619:
616:
613:
610:
607:
604:
601:
598:
595:
592:
589:
586:
583:
580:
577:
574:
571:
568:
565:
562:
559:
556:
553:
550:
547:
544:
541:
538:
535:
532:
529:
526:
523:
520:
517:
514:
511:
508:
505:
502:
499:
496:
493:
490:
487:
484:
481:
478:
475:
472:
469:
466:
463:
460:
457:
454:
451:
448:
445:
442:
439:
436:
433:
430:
427:
424:
421:
418:
415:
412:
409:
406:
403:
400:
397:
394:
391:
388:
385:
382:
379:
376:
333:
306:. In the 1990s,
221:. Coq is not an
184:
181:
179:
130:Operating system
114:
111:
109:
107:
89:
87:
86:3 September 2024
82:
78:
57:
55:
50:
29:
22:
18:
2608:
2607:
2603:
2602:
2601:
2599:
2598:
2597:
2538:
2537:
2536:
2531:
2489:
2468:
2444:Thierry Coquand
2435:
2375:
2366:
2352:
2293:
2290:Theorem provers
2284:
2209:
2179:
2158:
2115:
2060:
2057:Implementations
2042:
2036:
2004:by Andrej Bauer
1885:
1884:
1881:
1876:
1875:
1860:
1834:
1830:
1815:
1791:
1787:
1778:
1776:
1768:
1767:
1763:
1756:
1730:
1726:
1717:
1715:
1707:
1706:
1702:
1695:
1671:
1667:
1649:10.1145/3236773
1628:
1624:
1615:
1613:
1611:bbchallenge.org
1605:
1604:
1600:
1591:
1589:
1580:
1579:
1575:
1566:
1564:
1555:
1554:
1550:
1529:
1525:
1510:
1509:
1505:
1478:
1474:
1448:
1442:
1438:
1403:
1399:
1386:
1382:
1373:
1369:
1359:
1357:
1353:
1352:
1348:
1339:
1337:
1327:
1326:
1322:
1312:
1310:
1308:
1292:
1288:
1281:
1277:
1262:
1261:
1257:
1247:
1245:
1237:
1236:
1232:
1223:
1222:
1218:
1213:
1180:
1175:
1173:
1166:
1159:
1156:
1144:Kleene algebras
1136:
1135:
1132:
1129:
1126:
1123:
1120:
1117:
1114:
1111:
1108:
1105:
1102:
1099:
1096:
1093:
1090:
1087:
1084:
1081:
1078:
1075:
1072:
1069:
1066:
1063:
1060:
1057:
1054:
1051:
1048:
1045:
1042:
1039:
1036:
1033:
1030:
1027:
1024:
1021:
1018:
1015:
1012:
1009:
1006:
1003:
1000:
997:
994:
991:
988:
985:
982:
979:
976:
973:
970:
967:
964:
961:
958:
955:
952:
949:
918:
916:Tactic language
879:
873:
853:
838:inductive types
799:
794:
789:
788:
785:
782:
779:
776:
773:
770:
767:
764:
761:
758:
755:
752:
749:
746:
743:
740:
737:
734:
731:
728:
725:
722:
719:
716:
713:
710:
707:
704:
701:
698:
695:
692:
689:
686:
683:
680:
677:
674:
671:
668:
665:
662:
659:
656:
653:
650:
647:
644:
641:
638:
635:
632:
629:
626:
623:
620:
617:
614:
611:
608:
605:
602:
599:
596:
593:
590:
587:
584:
581:
578:
575:
572:
569:
566:
563:
560:
557:
554:
551:
548:
545:
542:
539:
536:
533:
530:
527:
524:
521:
518:
515:
512:
509:
506:
503:
500:
497:
494:
491:
488:
485:
482:
479:
476:
473:
470:
467:
464:
461:
458:
455:
452:
449:
446:
443:
440:
437:
434:
431:
428:
425:
422:
419:
416:
413:
410:
407:
404:
401:
398:
395:
392:
389:
386:
383:
380:
377:
374:
270:
242:Thierry Coquand
176:
155:Proof assistant
104:
90:
85:
83:
80:
53:
51:
48:
47:1 May 1989
44:Initial release
17:
16:Proof assistant
12:
11:
5:
2606:
2596:
2595:
2590:
2585:
2580:
2575:
2570:
2568:OCaml software
2565:
2560:
2555:
2550:
2533:
2532:
2530:
2481:
2479:= discontinued
2473:
2470:
2469:
2467:
2466:
2464:Simon Thompson
2461:
2459:Frank Pfenning
2456:
2451:
2446:
2440:
2437:
2436:
2434:
2428:
2422:
2416:
2410:
2404:
2401:Damien Doligez
2398:
2392:
2390:
2383:
2377:
2376:
2369:
2367:
2365:
2364:
2357:
2354:
2353:
2351:
2350:
2344:
2338:
2331:
2326:
2320:
2319:
2318:
2306:
2299:
2297:
2286:
2285:
2283:
2278:
2272:
2266:
2260:
2254:
2248:
2242:
2236:
2230:
2225:
2219:
2217:
2211:
2210:
2208:
2207:
2201:
2196:
2191:
2184:
2181:
2180:
2178:
2177:
2170:
2168:
2160:
2159:
2157:
2156:
2150:
2144:
2139:
2134:
2125:
2123:
2117:
2116:
2114:
2113:
2112:
2111:
2105:
2099:
2093:
2087:
2075:
2073:
2064:
2050:
2044:
2043:
2035:
2034:
2027:
2020:
2012:
2006:
2005:
1999:
1985:
1984:
1980:
1979:
1973:
1963:
1957:
1950:
1949:
1945:
1944:
1935:
1930:
1925:
1919:
1914:
1908:
1902:
1892:
1880:
1879:External links
1877:
1874:
1873:
1858:
1828:
1813:
1785:
1761:
1754:
1724:
1700:
1693:
1665:
1622:
1598:
1573:
1548:
1523:
1503:
1472:
1436:
1397:
1380:
1367:
1346:
1320:
1306:
1286:
1275:
1255:
1230:
1215:
1214:
1212:
1209:
1208:
1207:
1202:
1197:
1192:
1186:
1185:
1171:
1155:
1152:
948:
917:
914:
913:
912:
902:
896:
890:
872:
869:
861:
860:
857:
850:
847:
841:
798:
795:
793:
790:
373:
315:with a bit of
269:
266:
229:) and various
186:
185:
174:
170:
169:
164:
158:
157:
152:
146:
145:
142:
138:
137:
135:Cross-platform
132:
126:
125:
120:
116:
115:
102:
96:
95:
92:
91:
72:
70:
68:Stable release
64:
63:
60:
59:
58:(version 4.10)
45:
41:
40:
37:
31:
30:
20:Coq (software)
15:
9:
6:
4:
3:
2:
2605:
2594:
2591:
2589:
2588:1989 software
2586:
2584:
2581:
2579:
2576:
2574:
2571:
2569:
2566:
2564:
2561:
2559:
2556:
2554:
2551:
2549:
2546:
2545:
2543:
2529:
2528:
2519:
2518:
2509:
2508:
2499:
2498:
2493:
2488:
2487:
2482:
2480:
2477:
2474:
2471:
2465:
2462:
2460:
2457:
2455:
2452:
2450:
2447:
2445:
2442:
2441:
2432:
2429:
2427:(Extended ML)
2426:
2423:
2420:
2417:
2415:(Caml, OCaml)
2414:
2411:
2408:
2405:
2402:
2399:
2396:
2393:
2391:
2387:
2384:
2382:
2378:
2373:
2362:
2359:
2358:
2348:
2345:
2342:
2339:
2337:
2336:
2332:
2330:
2327:
2324:
2321:
2316:
2313:
2312:
2310:
2307:
2304:
2301:
2300:
2298:
2296:
2291:
2287:
2282:
2279:
2276:
2273:
2270:
2267:
2264:
2261:
2258:
2255:
2252:
2249:
2246:
2243:
2240:
2237:
2234:
2231:
2229:
2226:
2223:
2220:
2218:
2216:
2212:
2205:
2202:
2200:
2197:
2195:
2192:
2189:
2186:
2185:
2175:
2172:
2171:
2169:
2167:
2166:
2161:
2154:
2151:
2148:
2145:
2143:
2140:
2138:
2137:Concurrent ML
2135:
2132:
2131:
2127:
2126:
2124:
2122:
2118:
2109:
2106:
2103:
2100:
2097:
2094:
2091:
2088:
2086:
2083:
2082:
2080:
2077:
2076:
2074:
2072:
2068:
2065:
2063:
2058:
2054:
2051:
2049:
2045:
2040:
2033:
2028:
2026:
2021:
2019:
2014:
2013:
2010:
2003:
2000:
1998:
1994:
1990:
1987:
1986:
1982:
1981:
1977:
1974:
1971:
1967:
1964:
1961:
1958:
1955:
1952:
1951:
1947:
1946:
1943:
1939:
1936:
1934:
1931:
1929:
1926:
1923:
1920:
1918:
1915:
1912:
1909:
1906:
1903:
1900:
1896:
1893:
1888:
1883:
1882:
1869:
1865:
1861:
1855:
1851:
1847:
1843:
1839:
1832:
1824:
1820:
1816:
1810:
1806:
1802:
1798:
1797:
1789:
1775:
1771:
1765:
1757:
1751:
1747:
1743:
1739:
1735:
1728:
1714:
1710:
1704:
1696:
1690:
1686:
1682:
1678:
1677:
1669:
1660:
1655:
1650:
1645:
1641:
1637:
1633:
1626:
1612:
1608:
1602:
1587:
1583:
1577:
1563:on 2016-11-19
1562:
1558:
1552:
1544:
1540:
1536:
1535:
1527:
1519:
1518:
1513:
1507:
1499:
1495:
1492:(2): 95–152.
1491:
1487:
1483:
1476:
1468:
1464:
1460:
1456:
1455:
1447:
1440:
1432:
1428:
1424:
1420:
1416:
1412:
1408:
1401:
1394:
1390:
1384:
1377:
1371:
1356:
1350:
1336:
1335:
1330:
1324:
1309:
1307:9783319948218
1303:
1299:
1298:
1290:
1284:
1279:
1271:
1270:
1265:
1259:
1244:
1240:
1234:
1226:
1220:
1216:
1206:
1203:
1201:
1198:
1196:
1193:
1191:
1188:
1187:
1183:
1172:
1169:
1163:
1158:
1151:
1149:
1145:
1141:
946:
944:
940:
936:
932:
928:
923:
910:
906:
903:
900:
897:
894:
891:
888:
884:
881:
880:
878:
868:
866:
858:
851:
848:
846:
842:
839:
835:
831:
830:
829:
827:
823:
819:
815:
811:
807:
803:
371:
368:
366:
361:
357:
352:
349:
345:
341:
337:
332:
331:
324:
322:
318:
314:
309:
305:
301:
297:
293:
289:
285:
282:
278:
275:
265:
262:
257:
255:
251:
247:
243:
239:
234:
232:
228:
224:
220:
216:
212:
208:
204:
200:
192:
183:
175:
171:
168:
165:
163:
159:
156:
153:
151:
147:
143:
139:
136:
133:
131:
127:
124:
121:
117:
113:
103:
101:
97:
93:
77:
71:
69:
65:
61:
46:
42:
38:
36:
32:
28:
23:
2525:
2515:
2505:
2495:
2483:
2478:
2475:
2425:Don Sannella
2419:Robin Milner
2413:Xavier Leroy
2333:
2302:
2281:SLAM project
2165:Dependent ML
2163:
2128:
1993:Andrew Appel
1933:Math Classes
1891:, in English
1841:
1831:
1795:
1788:
1777:. Retrieved
1774:coq.inria.fr
1773:
1764:
1737:
1727:
1716:. Retrieved
1713:coq.inria.fr
1712:
1703:
1675:
1668:
1639:
1635:
1625:
1614:. Retrieved
1610:
1601:
1590:. Retrieved
1588:. 2024-07-02
1585:
1576:
1565:. Retrieved
1561:the original
1551:
1533:
1526:
1515:
1506:
1489:
1485:
1475:
1458:
1452:
1439:
1414:
1410:
1400:
1383:
1370:
1358:. Retrieved
1349:
1338:. Retrieved
1332:
1323:
1311:. Retrieved
1296:
1289:
1278:
1267:
1258:
1246:. Retrieved
1242:
1233:
1219:
1140:empty theory
1137:
921:
919:
908:
862:
852:An improved
800:
792:Notable uses
369:
353:
325:
281:higher-order
271:
260:
258:
235:
233:procedures.
198:
197:
141:Available in
73:8.20.0
35:Developer(s)
2407:GĂ©rard Huet
2142:Extended ML
2121:Standard ML
2041:programming
1954:The Coq'Art
939:commutative
935:associative
933:axioms via
905:Busy beaver
777:reflexivity
762:reflexivity
411:reflexivity
323:mechanism.
284:type theory
246:GĂ©rard Huet
2542:Categories
2155:° (SML/NJ)
1779:2023-12-04
1718:2023-12-04
1616:2024-07-02
1592:2024-07-02
1567:2012-09-25
1340:2019-05-08
1313:21 October
1300:Springer.
1211:References
875:See also:
227:procedures
119:Written in
100:Repository
54:1989-05-01
2397:(Lazy ML)
2389:Designers
2381:Community
2315:HOL Light
2257:Marionnet
1983:Tutorials
1948:Textbooks
1911:Alectryon
1431:0956-7968
1148:geometric
810:Cambridge
326:The name
256:for Coq.
2431:Don Syme
2323:Isabelle
2222:Alt-Ergo
2062:dialects
2048:Software
1942:Open Hub
1917:Coq Wiki
1868:11238876
1154:See also
943:integers
931:semiring
883:CompCert
865:CeCILL-B
738:destruct
435:Fixpoint
308:ENS Lyon
268:Overview
240:awarded
231:decision
167:LGPLv2.1
2476:Italics
2403:(OCaml)
2361:GeneWeb
2275:Semgrep
2245:Frama-C
2199:MacroML
2194:Lazy ML
2188:Futhark
1823:3566183
1467:2463991
1248:3 March
1150:goals.
968:Z_scope
950:Require
922:tactics
824:of the
814:England
744:is_even
720:rewrite
690:is_even
675:is_even
639:is_even
615:is_even
591:is_even
555:is_even
531:is_even
504:is_even
438:is_even
417:Require
336:rooster
334:means '
321:plug-in
209:of its
173:Website
162:License
144:English
84: (
52: (
2409:(Caml)
2341:Matita
2269:Poplog
2233:Camlp4
2228:Astrée
2108:Reason
2102:JoCaml
1972:et al.
1899:GitHub
1866:
1856:
1821:
1811:
1752:
1691:
1517:GitHub
1465:
1429:
1360:21 May
1334:GitHub
1304:
1269:GitHub
1243:GitHub
1118:intros
977:forall
956:ZArith
953:Import
660:forall
618:n'
600:n'
579:n'
576:forall
507:n'
492:n'
420:Import
393:unfold
387:intros
340:French
302:, and
201:is an
180:.inria
106:github
2347:Twelf
2263:MTASC
2147:MLton
2130:Alice
2079:OCaml
1864:S2CID
1819:S2CID
1449:(PDF)
965:Scope
909:BB(5)
836:, on
818:INRIA
771:simpl
756:simpl
723:->
711:intro
705:Proof
651:Lemma
630:Proof
624:false
567:Lemma
546:Proof
522:Lemma
513:false
495:=>
480:=>
465:match
423:Arith
338:' in
313:OCaml
288:INRIA
123:OCaml
2497:Book
2484:° =
2433:(F#)
2421:(ML)
2329:LEGO
2251:Haxe
2239:FFTW
2071:Caml
1854:ISBN
1809:ISBN
1750:ISBN
1689:ISBN
1427:ISSN
1362:2019
1315:2018
1302:ISBN
1250:2023
1124:ring
974:Goal
962:Open
927:ring
684:negb
540:true
483:true
471:with
459:bool
429:Bool
405:name
402:fold
396:name
381:name
375:Ltac
304:CNRS
236:The
150:Type
112:/coq
110:/coq
108:.com
2309:HOL
2303:Coq
2174:ATS
2085:Eff
1995:at
1940:at
1938:Coq
1897:on
1895:Coq
1846:doi
1801:doi
1742:doi
1681:doi
1654:hdl
1644:doi
1539:doi
1494:doi
1419:doi
1130:Qed
929:or
854:set
808:in
804:of
783:Qed
702:)).
669:nat
645:Qed
609:eqb
585:nat
561:Qed
516:end
498:eqb
450:nat
426:Nat
356:hen
330:coq
261:coq
199:Coq
182:.fr
178:coq
2544::
2311:°
2204:Ur
2096:F#
2090:F*
2081:°
2039:ML
1862:.
1852:.
1817:.
1807:.
1772:.
1748:.
1711:.
1687:.
1652:.
1638:.
1634:.
1609:.
1584:.
1514:.
1488:.
1484:.
1463:MR
1459:55
1457:.
1451:.
1425:.
1417:.
1415:32
1413:.
1409:.
1391:.
1331:.
1266:.
1241:.
812:,
750:).
735:).
462::=
384::=
367:.
298:,
294:,
248:,
244:,
2363:°
2349:°
2343:°
2325:°
2317:°
2305:°
2292:,
2277:°
2271:°
2265:°
2259:°
2253:°
2247:°
2241:°
2235:°
2224:°
2206:°
2190:°
2176:°
2149:°
2133:°
2110:°
2104:°
2098:°
2092:°
2059:,
2031:e
2024:t
2017:v
1870:.
1848::
1825:.
1803::
1782:.
1758:.
1744::
1721:.
1697:.
1683::
1662:.
1656::
1646::
1640:2
1619:.
1595:.
1570:.
1545:.
1541::
1520:.
1500:.
1496::
1490:3
1469:.
1433:.
1421::
1395:.
1378:.
1364:.
1343:.
1317:.
1272:.
1252:.
1133:.
1127:.
1121:;
1115:.
1112:c
1109:*
1106:b
1103:*
1100:2
1097:+
1094:c
1091:*
1088:a
1085:*
1082:2
1079:+
1076:b
1073:*
1070:a
1067:*
1064:2
1061:+
1058:c
1055:*
1052:c
1049:+
1046:2
1043:^
1040:b
1037:+
1034:a
1031:*
1028:a
1025:=
1022:2
1019:^
1016:)
1013:c
1010:+
1007:b
1004:+
1001:a
998:(
995:,
992:Z
989::
986:c
983:b
980:a
971:.
959:.
937:-
786:.
780:.
774:.
768:*
765:.
759:.
753:*
747:n
741:(
732:n
726:(
717:.
714:n
708:.
699:n
696:S
693:(
687:(
681:=
678:n
672:,
666::
663:n
657::
648:.
642:.
633:.
627:.
621:)
612:(
606:=
603:)
597:S
594:(
588:,
582::
573::
564:.
558:.
549:.
543:.
537:=
534:0
528::
519:.
510:)
501:(
489:S
486:|
477:0
474:|
468:n
456::
453:)
447::
444:n
441:(
432:.
414:.
408:;
399:;
390:;
317:C
88:)
56:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
