2337:
1985:
2332:{\displaystyle {\begin{array}{ccll}A\Rightarrow B&\equiv &\forall x:A.B&(x\notin B)\\A\wedge B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow B\Rightarrow C)\Rightarrow C&\\A\vee B&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)\Rightarrow (B\Rightarrow C)\Rightarrow C&\\\neg A&\equiv &\forall C:\mathbf {P} .(A\Rightarrow C)&\\\exists x:A.B&\equiv &\forall C:\mathbf {P} .(\forall x:A.(B\Rightarrow C))\Rightarrow C&\end{array}}}
607:
1739:
1950:
1608:
1855:
2465:
1297:
2400:
1430:
1498:
789:
510:
1618:
1025:
1865:
1374:
1508:
889:
843:
1749:
1337:
492:
449:
2796:
1133:
1111:
689:
665:
232:
204:
271:
2520:
2493:
1977:
2575:
1063:
953:
343:
2548:
1089:
1231:
1211:
1188:
1168:
929:
909:
406:
386:
366:
314:
294:
2409:
108:
2899:
2356:
1391:
1242:
104:. It is possible within CoC to define functions from terms to terms, as well as terms to types, types to types, and types to terms.
1440:
2826:
710:
2852:
602:{\displaystyle e::=\mathbf {T} \mid \mathbf {P} \mid x\mid e\,e\mid \lambda x{\mathbin {:}}e.e\mid \forall x{\mathbin {:}}e.e}
2871:
1734:{\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash N:B \over {\Gamma \vdash (\lambda x:A.N):(\forall x:A.B)}}}
935:
The valid judgments for the calculus of constructions are derivable from a set of inference rules. In the following, we use
150:
51:
2726:
1945:{\displaystyle {\Gamma \vdash M:A\qquad \qquad A=_{\beta }B\qquad \qquad \Gamma \vdash B:K \over {\Gamma \vdash M:B}}}
958:
2613:
54:
1959:
The calculus of constructions has very few basic operators: the only logical operator for forming propositions is
2904:
1603:{\displaystyle {\Gamma \vdash A:K\qquad \qquad \Gamma ,x:A\vdash B:L \over {\Gamma \vdash (\forall x:A.B):L}}}
1850:{\displaystyle {\Gamma \vdash M:(\forall x:A.B)\qquad \qquad \Gamma \vdash N:A \over {\Gamma \vdash MN:B}}}
2813:
138:
848:
802:
1342:
154:
130:. As features were added (or possible liabilities removed) to the theory, they became available in Coq.
89:
1310:
501:
2641:
2909:
2618:
456:
413:
162:
47:
2664:"A Proof of Strong Normalization for the Theory of Constructions Using a Kripke-Like Interpretation"
2817:
2766:
2718:
2347:
The basic data types used in computer science can be defined within the calculus of constructions:
2647:
1116:
1094:
672:
648:
215:
187:
244:
166:
20:
2637:
2499:
2472:
2867:
2584:. However, additional problems arise from propositional extensionality and proof irrelevance.
1962:
165:. The calculus of constructions extends this isomorphism to proofs in the full intuitionistic
158:
2554:
1030:
938:
2735:
2681:
2593:
1990:
24:
169:, which includes proofs of quantified statements (which we will also call "propositions").
2710:
2581:
319:
127:
97:
93:
77:
62:
40:
2527:
1068:
2714:
2608:
1216:
1196:
1173:
1138:
914:
894:
391:
371:
351:
299:
279:
124:
69:
58:
1979:. However, this one operator is sufficient to define all the other logical operators:
2893:
2859:
2740:
1191:
2833:
2877:
2809:
2460:{\displaystyle \forall A:\mathbf {P} .(A\Rightarrow A)\Rightarrow A\Rightarrow A}
68:
Some of its variants include the calculus of inductive constructions (which adds
2663:
2598:
101:
73:
44:
36:
76:), and the predicative calculus of inductive constructions (which removes some
112:
181:
in the calculus of constructions is constructed using the following rules:
57:. For this second reason, the CoC and its variants have been the basis for
2751:
2603:
134:
149:
The calculus of constructions can be considered an extension of the
2853:"Induction Principles Formalized in the Calculus of Constructions"
2757:
2580:
Note that
Booleans and Naturals are defined in the same way as in
2395:{\displaystyle \forall A:\mathbf {P} .A\Rightarrow A\Rightarrow A}
1425:{\displaystyle {{} \over \Gamma \vdash \mathbf {P} :\mathbf {T} }}
133:
Variants of the CoC are used in other proof assistants, such as
1292:{\displaystyle {\frac {\Gamma \vdash A:B}{\Gamma '\vdash C:D}}}
1493:{\displaystyle {{} \over {\Gamma ,x:A,\Gamma '\vdash x:A}}}
72:), the calculus of (co)inductive constructions (which adds
784:{\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots \vdash t:B}
612:
The calculus of constructions has five kinds of objects:
153:. The Curry–Howard isomorphism associates a term in the
2769:
2763:
Note terminology is rather different. For instance, (
2557:
2530:
2502:
2475:
2412:
2359:
1988:
1965:
1868:
1752:
1621:
1511:
1443:
1394:
1345:
1313:
1245:
1219:
1199:
1176:
1141:
1119:
1097:
1071:
1033:
961:
941:
917:
897:
851:
805:
713:
675:
651:
513:
459:
416:
394:
374:
354:
322:
302:
282:
247:
218:
190:
2790:
2569:
2542:
2514:
2487:
2459:
2394:
2331:
1971:
1944:
1849:
1733:
1602:
1492:
1424:
1368:
1331:
1291:
1225:
1205:
1182:
1162:
1127:
1105:
1083:
1057:
1019:
947:
923:
903:
883:
837:
783:
683:
659:
601:
486:
443:
408:is a variable, then the following are also terms:
400:
380:
360:
337:
308:
288:
265:
226:
198:
2810:"Variants of the Basic Calculus of Constructions"
1381:Inference rules for the calculus of constructions
2662:Coquand, Thierry; Gallier, Jean H. (July 1990).
1020:{\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }
639:, which are functions that return propositions;
700:The calculus of constructions allows proving
8:
2682:"Standard Library | The Coq Proof Assistant"
1170:to mean the result of substituting the term
2808:Bunder, M. W.; Seldin, Jonathan P. (2004).
145:The basics of the calculus of constructions
96:. It is well known for being at the top of
2864:Programming of Future Generation Computers
2768:
2748:Also available freely accessible online:
2739:
2556:
2529:
2501:
2474:
2422:
2411:
2369:
2358:
2274:
2212:
2138:
2073:
1989:
1987:
1964:
1923:
1896:
1869:
1867:
1810:
1753:
1751:
1670:
1622:
1620:
1560:
1512:
1510:
1448:
1446:
1444:
1442:
1414:
1406:
1397:
1395:
1393:
1344:
1312:
1246:
1244:
1236:An inference rule is written in the form
1218:
1198:
1175:
1140:
1120:
1118:
1098:
1096:
1070:
1032:
1005:
992:
979:
966:
960:
940:
916:
896:
869:
856:
850:
823:
810:
804:
757:
744:
731:
718:
712:
691:itself, which is the type of large types.
676:
674:
652:
650:
584:
583:
559:
558:
545:
528:
520:
512:
458:
415:
393:
373:
353:
321:
301:
281:
246:
219:
217:
191:
189:
123:The CoC has been developed alongside the
955:to mean a sequence of type assignments
2750:Coquand, Thierry; Huet, GĂ©rard (1986).
2630:
2640:, and basic standard libraries :
16:Type theory created by Thierry Coquand
2827:"Calculus of Inductive Constructions"
795:which can be read as the implication
645:, which are the types of predicates (
7:
500:In other words, the term syntax, in
2866:. North-Holland. pp. 205–216.
2638:Calculus of Inductive Constructions
884:{\displaystyle A_{1},A_{2},\ldots }
838:{\displaystyle x_{1},x_{2},\ldots }
2770:
2413:
2360:
2285:
2265:
2240:
2203:
2190:
2129:
2064:
2009:
1966:
1924:
1907:
1872:
1811:
1794:
1771:
1756:
1707:
1671:
1642:
1625:
1570:
1561:
1532:
1515:
1468:
1449:
1400:
1369:{\displaystyle \Gamma '\vdash C:D}
1347:
1314:
1267:
1249:
942:
619:, which are terms whose types are
577:
463:
163:intuitionistic propositional logic
14:
2885:— An application of the CoC
1332:{\displaystyle \Gamma \vdash A:B}
2423:
2370:
2275:
2213:
2139:
2074:
1415:
1407:
1339:is a valid judgment, then so is
1121:
1099:
677:
653:
529:
521:
238:, the type of all propositions);
220:
192:
2719:"The Calculus of Constructions"
1906:
1905:
1888:
1887:
1793:
1792:
1641:
1640:
1531:
1530:
667:is an example of a large type);
487:{\displaystyle (\forall x:A.B)}
444:{\displaystyle (\lambda x:A.B)}
2760:, Centre de Rocquencourt. 530.
2451:
2445:
2442:
2436:
2430:
2386:
2380:
2318:
2315:
2312:
2306:
2300:
2282:
2232:
2226:
2220:
2179:
2176:
2170:
2164:
2161:
2158:
2152:
2146:
2102:
2099:
2093:
2087:
2081:
2041:
2029:
1996:
1841:
1829:
1789:
1768:
1725:
1704:
1698:
1677:
1588:
1567:
1157:
1145:
481:
460:
438:
417:
332:
323:
1:
2900:Dependently typed programming
2791:{\displaystyle \forall x:A.B}
2753:The calculus of constructions
2741:10.1016/0890-5401(88)90005-3
1128:{\displaystyle \mathbf {T} }
1106:{\displaystyle \mathbf {P} }
684:{\displaystyle \mathbf {T} }
660:{\displaystyle \mathbf {P} }
227:{\displaystyle \mathbf {P} }
199:{\displaystyle \mathbf {T} }
155:simply typed lambda calculus
2727:Information and Computation
266:{\displaystyle x,y,\ldots }
2926:
2825:Frade, Maria JoĂŁo (2009).
2614:Intuitionistic type theory
1955:Defining logical operators
845:have, respectively, types
629:, which are also known as
88:The CoC is a higher-order
55:foundation for mathematics
2515:{\displaystyle A\wedge B}
2488:{\displaystyle A\times B}
92:, initially developed by
43:. It can serve as both a
29:calculus of constructions
1972:{\displaystyle \forall }
151:Curry–Howard isomorphism
2668:Technical Reports (Cis)
2570:{\displaystyle A\vee B}
1058:{\displaystyle A,B,C,D}
948:{\displaystyle \Gamma }
234:is a term (also called
206:is a term (also called
2792:
2571:
2544:
2516:
2489:
2461:
2396:
2333:
1973:
1946:
1851:
1735:
1604:
1494:
1426:
1370:
1333:
1293:
1227:
1207:
1184:
1164:
1129:
1107:
1085:
1059:
1021:
949:
925:
905:
885:
839:
785:
685:
661:
603:
488:
445:
402:
382:
362:
339:
316:are terms, then so is
310:
290:
267:
228:
200:
2851:Huet, GĂ©rard (1988).
2793:
2572:
2545:
2517:
2490:
2462:
2397:
2334:
1974:
1947:
1852:
1736:
1605:
1495:
1427:
1371:
1334:
1294:
1228:
1208:
1185:
1165:
1130:
1108:
1086:
1060:
1022:
950:
926:
906:
886:
840:
786:
686:
662:
604:
489:
446:
403:
383:
363:
340:
311:
291:
268:
229:
201:
90:typed lambda calculus
2767:
2756:(Technical report).
2619:Homotopy type theory
2555:
2528:
2500:
2473:
2410:
2357:
1986:
1963:
1866:
1750:
1619:
1509:
1441:
1392:
1343:
1311:
1243:
1217:
1197:
1174:
1139:
1117:
1095:
1069:
1031:
959:
939:
915:
895:
849:
803:
711:
673:
649:
511:
457:
414:
392:
372:
352:
338:{\displaystyle (AB)}
320:
300:
280:
245:
216:
188:
109:strongly normalizing
48:programming language
2543:{\displaystyle A+B}
2343:Defining data types
1084:{\displaystyle K,L}
1065:to mean terms; and
2788:
2567:
2540:
2512:
2485:
2457:
2392:
2329:
2327:
1969:
1942:
1847:
1731:
1600:
1490:
1422:
1366:
1329:
1289:
1223:
1203:
1180:
1160:
1125:
1103:
1081:
1055:
1017:
945:
921:
901:
881:
835:
781:
681:
657:
599:
484:
441:
398:
378:
358:
335:
306:
286:
263:
224:
196:
167:predicate calculus
21:mathematical logic
1940:
1845:
1729:
1598:
1488:
1420:
1287:
1226:{\displaystyle B}
1206:{\displaystyle x}
1183:{\displaystyle N}
1163:{\displaystyle B}
1135:. We shall write
924:{\displaystyle B}
904:{\displaystyle t}
401:{\displaystyle x}
381:{\displaystyle B}
361:{\displaystyle A}
309:{\displaystyle B}
289:{\displaystyle A}
159:natural-deduction
2917:
2884:
2882:
2876:. Archived from
2858:. In Fuchi, K.;
2857:
2847:
2845:
2844:
2838:
2832:. Archived from
2831:
2821:
2797:
2795:
2794:
2789:
2761:
2745:
2743:
2723:
2711:Coquand, Thierry
2696:
2695:
2693:
2692:
2678:
2672:
2671:
2659:
2653:
2650:
2644:
2635:
2594:Pure type system
2576:
2574:
2573:
2568:
2549:
2547:
2546:
2541:
2521:
2519:
2518:
2513:
2494:
2492:
2491:
2486:
2466:
2464:
2463:
2458:
2426:
2401:
2399:
2398:
2393:
2373:
2338:
2336:
2335:
2330:
2328:
2325:
2278:
2236:
2216:
2186:
2142:
2109:
2077:
1978:
1976:
1975:
1970:
1951:
1949:
1948:
1943:
1941:
1939:
1922:
1901:
1900:
1870:
1856:
1854:
1853:
1848:
1846:
1844:
1809:
1754:
1740:
1738:
1737:
1732:
1730:
1728:
1669:
1623:
1609:
1607:
1606:
1601:
1599:
1597:
1559:
1513:
1499:
1497:
1496:
1491:
1489:
1487:
1474:
1447:
1445:
1431:
1429:
1428:
1423:
1421:
1419:
1418:
1410:
1398:
1396:
1375:
1373:
1372:
1367:
1353:
1338:
1336:
1335:
1330:
1298:
1296:
1295:
1290:
1288:
1286:
1273:
1264:
1247:
1232:
1230:
1229:
1224:
1212:
1210:
1209:
1204:
1189:
1187:
1186:
1181:
1169:
1167:
1166:
1161:
1134:
1132:
1131:
1126:
1124:
1112:
1110:
1109:
1104:
1102:
1090:
1088:
1087:
1082:
1064:
1062:
1061:
1056:
1026:
1024:
1023:
1018:
1010:
1009:
997:
996:
984:
983:
971:
970:
954:
952:
951:
946:
930:
928:
927:
922:
910:
908:
907:
902:
890:
888:
887:
882:
874:
873:
861:
860:
844:
842:
841:
836:
828:
827:
815:
814:
790:
788:
787:
782:
762:
761:
749:
748:
736:
735:
723:
722:
702:typing judgments
690:
688:
687:
682:
680:
666:
664:
663:
658:
656:
608:
606:
605:
600:
589:
588:
564:
563:
532:
524:
502:Backus–Naur form
493:
491:
490:
485:
450:
448:
447:
442:
407:
405:
404:
399:
387:
385:
384:
379:
367:
365:
364:
359:
344:
342:
341:
336:
315:
313:
312:
307:
295:
293:
292:
287:
272:
270:
269:
264:
233:
231:
230:
225:
223:
205:
203:
202:
197:
195:
63:proof assistants
25:computer science
2925:
2924:
2920:
2919:
2918:
2916:
2915:
2914:
2905:Lambda calculus
2890:
2889:
2888:
2880:
2874:
2855:
2850:
2842:
2840:
2836:
2829:
2824:
2807:
2765:
2764:
2762:
2749:
2734:(2–3): 95–120.
2721:
2709:
2705:
2700:
2699:
2690:
2688:
2680:
2679:
2675:
2661:
2660:
2656:
2648:
2642:
2636:
2632:
2627:
2590:
2582:Church encoding
2553:
2552:
2526:
2525:
2524:Disjoint union
2498:
2497:
2471:
2470:
2408:
2407:
2355:
2354:
2345:
2326:
2324:
2263:
2258:
2237:
2235:
2201:
2196:
2187:
2185:
2127:
2122:
2110:
2108:
2062:
2057:
2045:
2044:
2027:
2007:
2002:
1984:
1983:
1961:
1960:
1957:
1892:
1871:
1864:
1863:
1755:
1748:
1747:
1624:
1617:
1616:
1514:
1507:
1506:
1467:
1439:
1438:
1399:
1390:
1389:
1383:
1346:
1341:
1340:
1309:
1308:
1266:
1265:
1248:
1241:
1240:
1215:
1214:
1195:
1194:
1172:
1171:
1137:
1136:
1115:
1114:
1093:
1092:
1091:to mean either
1067:
1066:
1029:
1028:
1001:
988:
975:
962:
957:
956:
937:
936:
913:
912:
893:
892:
865:
852:
847:
846:
819:
806:
801:
800:
753:
740:
727:
714:
709:
708:
698:
671:
670:
647:
646:
509:
508:
455:
454:
412:
411:
390:
389:
370:
369:
350:
349:
318:
317:
298:
297:
278:
277:
243:
242:
214:
213:
186:
185:
175:
147:
128:proof assistant
121:
94:Thierry Coquand
86:
78:impredicativity
70:inductive types
41:Thierry Coquand
17:
12:
11:
5:
2923:
2921:
2913:
2912:
2907:
2902:
2892:
2891:
2887:
2886:
2883:on 2015-07-01.
2872:
2848:
2822:
2818:10.1.1.88.9497
2805:
2804:
2803:
2798:) is written
2787:
2784:
2781:
2778:
2775:
2772:
2706:
2704:
2701:
2698:
2697:
2673:
2654:
2629:
2628:
2626:
2623:
2622:
2621:
2616:
2611:
2609:Dependent type
2606:
2601:
2596:
2589:
2586:
2578:
2577:
2566:
2563:
2560:
2550:
2539:
2536:
2533:
2522:
2511:
2508:
2505:
2495:
2484:
2481:
2478:
2467:
2456:
2453:
2450:
2447:
2444:
2441:
2438:
2435:
2432:
2429:
2425:
2421:
2418:
2415:
2405:
2402:
2391:
2388:
2385:
2382:
2379:
2376:
2372:
2368:
2365:
2362:
2352:
2344:
2341:
2340:
2339:
2323:
2320:
2317:
2314:
2311:
2308:
2305:
2302:
2299:
2296:
2293:
2290:
2287:
2284:
2281:
2277:
2273:
2270:
2267:
2264:
2262:
2259:
2257:
2254:
2251:
2248:
2245:
2242:
2239:
2238:
2234:
2231:
2228:
2225:
2222:
2219:
2215:
2211:
2208:
2205:
2202:
2200:
2197:
2195:
2192:
2189:
2188:
2184:
2181:
2178:
2175:
2172:
2169:
2166:
2163:
2160:
2157:
2154:
2151:
2148:
2145:
2141:
2137:
2134:
2131:
2128:
2126:
2123:
2121:
2118:
2115:
2112:
2111:
2107:
2104:
2101:
2098:
2095:
2092:
2089:
2086:
2083:
2080:
2076:
2072:
2069:
2066:
2063:
2061:
2058:
2056:
2053:
2050:
2047:
2046:
2043:
2040:
2037:
2034:
2031:
2028:
2026:
2023:
2020:
2017:
2014:
2011:
2008:
2006:
2003:
2001:
1998:
1995:
1992:
1991:
1968:
1956:
1953:
1938:
1935:
1932:
1929:
1926:
1921:
1918:
1915:
1912:
1909:
1904:
1899:
1895:
1891:
1886:
1883:
1880:
1877:
1874:
1843:
1840:
1837:
1834:
1831:
1828:
1825:
1822:
1819:
1816:
1813:
1808:
1805:
1802:
1799:
1796:
1791:
1788:
1785:
1782:
1779:
1776:
1773:
1770:
1767:
1764:
1761:
1758:
1727:
1724:
1721:
1718:
1715:
1712:
1709:
1706:
1703:
1700:
1697:
1694:
1691:
1688:
1685:
1682:
1679:
1676:
1673:
1668:
1665:
1662:
1659:
1656:
1653:
1650:
1647:
1644:
1639:
1636:
1633:
1630:
1627:
1596:
1593:
1590:
1587:
1584:
1581:
1578:
1575:
1572:
1569:
1566:
1563:
1558:
1555:
1552:
1549:
1546:
1543:
1540:
1537:
1534:
1529:
1526:
1523:
1520:
1517:
1486:
1483:
1480:
1477:
1473:
1470:
1466:
1463:
1460:
1457:
1454:
1451:
1417:
1413:
1409:
1405:
1402:
1382:
1379:
1378:
1377:
1365:
1362:
1359:
1356:
1352:
1349:
1328:
1325:
1322:
1319:
1316:
1301:
1300:
1285:
1282:
1279:
1276:
1272:
1269:
1263:
1260:
1257:
1254:
1251:
1222:
1202:
1179:
1159:
1156:
1153:
1150:
1147:
1144:
1123:
1101:
1080:
1077:
1074:
1054:
1051:
1048:
1045:
1042:
1039:
1036:
1016:
1013:
1008:
1004:
1000:
995:
991:
987:
982:
978:
974:
969:
965:
944:
933:
932:
920:
900:
880:
877:
872:
868:
864:
859:
855:
834:
831:
826:
822:
818:
813:
809:
793:
792:
780:
777:
774:
771:
768:
765:
760:
756:
752:
747:
743:
739:
734:
730:
726:
721:
717:
697:
694:
693:
692:
679:
668:
655:
640:
634:
624:
610:
609:
598:
595:
592:
587:
582:
579:
576:
573:
570:
567:
562:
557:
554:
551:
548:
544:
541:
538:
535:
531:
527:
523:
519:
516:
498:
497:
496:
495:
483:
480:
477:
474:
471:
468:
465:
462:
452:
440:
437:
434:
431:
428:
425:
422:
419:
397:
388:are terms and
377:
357:
346:
334:
331:
328:
325:
305:
285:
274:
262:
259:
256:
253:
250:
239:
222:
211:
194:
174:
171:
146:
143:
120:
117:
85:
84:General traits
82:
15:
13:
10:
9:
6:
4:
3:
2:
2922:
2911:
2908:
2906:
2903:
2901:
2898:
2897:
2895:
2879:
2875:
2869:
2865:
2861:
2854:
2849:
2839:on 2014-05-29
2835:
2828:
2823:
2819:
2815:
2811:
2806:
2801:
2785:
2782:
2779:
2776:
2773:
2759:
2755:
2754:
2747:
2746:
2742:
2737:
2733:
2729:
2728:
2720:
2716:
2712:
2708:
2707:
2702:
2687:
2683:
2677:
2674:
2669:
2665:
2658:
2655:
2651:
2645:
2639:
2634:
2631:
2624:
2620:
2617:
2615:
2612:
2610:
2607:
2605:
2602:
2600:
2597:
2595:
2592:
2591:
2587:
2585:
2583:
2564:
2561:
2558:
2551:
2537:
2534:
2531:
2523:
2509:
2506:
2503:
2496:
2482:
2479:
2476:
2468:
2454:
2448:
2439:
2433:
2427:
2419:
2416:
2406:
2403:
2389:
2383:
2377:
2374:
2366:
2363:
2353:
2350:
2349:
2348:
2342:
2321:
2309:
2303:
2297:
2294:
2291:
2288:
2279:
2271:
2268:
2260:
2255:
2252:
2249:
2246:
2243:
2229:
2223:
2217:
2209:
2206:
2198:
2193:
2182:
2173:
2167:
2155:
2149:
2143:
2135:
2132:
2124:
2119:
2116:
2113:
2105:
2096:
2090:
2084:
2078:
2070:
2067:
2059:
2054:
2051:
2048:
2038:
2035:
2032:
2024:
2021:
2018:
2015:
2012:
2004:
1999:
1993:
1982:
1981:
1980:
1954:
1952:
1936:
1933:
1930:
1927:
1919:
1916:
1913:
1910:
1902:
1897:
1893:
1889:
1884:
1881:
1878:
1875:
1861:
1857:
1838:
1835:
1832:
1826:
1823:
1820:
1817:
1814:
1806:
1803:
1800:
1797:
1786:
1783:
1780:
1777:
1774:
1765:
1762:
1759:
1745:
1741:
1722:
1719:
1716:
1713:
1710:
1701:
1695:
1692:
1689:
1686:
1683:
1680:
1674:
1666:
1663:
1660:
1657:
1654:
1651:
1648:
1645:
1637:
1634:
1631:
1628:
1614:
1610:
1594:
1591:
1585:
1582:
1579:
1576:
1573:
1564:
1556:
1553:
1550:
1547:
1544:
1541:
1538:
1535:
1527:
1524:
1521:
1518:
1504:
1500:
1484:
1481:
1478:
1475:
1471:
1464:
1461:
1458:
1455:
1452:
1436:
1432:
1411:
1403:
1387:
1380:
1363:
1360:
1357:
1354:
1350:
1326:
1323:
1320:
1317:
1306:
1305:
1304:
1283:
1280:
1277:
1274:
1270:
1261:
1258:
1255:
1252:
1239:
1238:
1237:
1234:
1220:
1200:
1193:
1192:free variable
1177:
1154:
1151:
1148:
1142:
1078:
1075:
1072:
1052:
1049:
1046:
1043:
1040:
1037:
1034:
1014:
1011:
1006:
1002:
998:
993:
989:
985:
980:
976:
972:
967:
963:
918:
898:
878:
875:
870:
866:
862:
857:
853:
832:
829:
824:
820:
816:
811:
807:
799:If variables
798:
797:
796:
778:
775:
772:
769:
766:
763:
758:
754:
750:
745:
741:
737:
732:
728:
724:
719:
715:
707:
706:
705:
703:
695:
669:
644:
641:
638:
635:
632:
628:
625:
622:
618:
615:
614:
613:
596:
593:
590:
585:
580:
574:
571:
568:
565:
560:
555:
552:
549:
546:
542:
539:
536:
533:
525:
517:
514:
507:
506:
505:
503:
478:
475:
472:
469:
466:
453:
435:
432:
429:
426:
423:
420:
410:
409:
395:
375:
355:
347:
329:
326:
303:
283:
275:
260:
257:
254:
251:
248:
240:
237:
212:
209:
184:
183:
182:
180:
172:
170:
168:
164:
160:
156:
152:
144:
142:
140:
136:
131:
129:
126:
118:
116:
114:
110:
105:
103:
99:
95:
91:
83:
81:
79:
75:
71:
66:
64:
60:
56:
53:
49:
46:
42:
38:
34:
30:
26:
22:
2878:the original
2863:
2841:. Retrieved
2834:the original
2799:
2752:
2731:
2725:
2715:Huet, GĂ©rard
2689:. Retrieved
2686:coq.inria.fr
2685:
2676:
2667:
2657:
2633:
2579:
2346:
1958:
1859:
1858:
1743:
1742:
1612:
1611:
1502:
1501:
1434:
1433:
1385:
1384:
1303:which means
1302:
1235:
1213:in the term
934:
891:, then term
794:
701:
699:
642:
636:
630:
627:propositions
626:
621:propositions
620:
616:
611:
499:
273:) are terms;
235:
207:
178:
176:
148:
132:
122:
111:, and hence
106:
87:
67:
52:constructive
32:
28:
18:
2910:Type theory
2599:Lambda cube
643:large types
631:small types
504:, is then:
241:Variables (
107:The CoC is
102:lambda cube
74:coinduction
39:created by
37:type theory
2894:Categories
2873:0444704108
2843:2013-03-03
2691:2020-08-08
2625:References
637:predicates
157:with each
113:consistent
98:Barendregt
61:and other
2860:Nivat, M.
2771:∀
2643:Datatypes
2562:∨
2507:∧
2480:×
2452:⇒
2446:⇒
2437:⇒
2414:∀
2387:⇒
2381:⇒
2361:∀
2319:⇒
2307:⇒
2286:∀
2266:∀
2261:≡
2241:∃
2227:⇒
2204:∀
2199:≡
2191:¬
2180:⇒
2171:⇒
2162:⇒
2153:⇒
2130:∀
2125:≡
2117:∨
2103:⇒
2094:⇒
2088:⇒
2065:∀
2060:≡
2052:∧
2036:∉
2010:∀
2005:≡
1997:⇒
1967:∀
1928:⊢
1925:Γ
1911:⊢
1908:Γ
1898:β
1876:⊢
1873:Γ
1815:⊢
1812:Γ
1798:⊢
1795:Γ
1772:∀
1760:⊢
1757:Γ
1708:∀
1681:λ
1675:⊢
1672:Γ
1658:⊢
1643:Γ
1629:⊢
1626:Γ
1571:∀
1565:⊢
1562:Γ
1548:⊢
1533:Γ
1519:⊢
1516:Γ
1476:⊢
1469:Γ
1450:Γ
1404:⊢
1401:Γ
1355:⊢
1348:Γ
1318:⊢
1315:Γ
1275:⊢
1268:Γ
1253:⊢
1250:Γ
1015:…
943:Γ
911:has type
879:…
833:…
770:⊢
767:…
696:Judgments
578:∀
575:∣
553:λ
550:∣
540:∣
534:∣
526:∣
464:∀
421:λ
261:…
161:proof in
2862:(eds.).
2814:CiteSeer
2717:(1988).
2604:System F
2588:See also
2469:Product
2404:Naturals
2351:Booleans
1472:′
1351:′
1271:′
1190:for the
2816::
2703:Sources
50:and as
35:) is a
2870:
2837:(talk)
617:proofs
135:Matita
27:, the
2881:(PDF)
2856:(PDF)
2830:(PDF)
2758:INRIA
2722:(PDF)
2670:: 14.
2649:Logic
173:Terms
119:Usage
45:typed
2868:ISBN
2646:and
1862:.
368:and
296:and
236:prop
208:type
179:term
139:Lean
137:and
23:and
2736:doi
1307:if
1113:or
518:::=
348:If
276:If
125:Coq
100:'s
80:).
59:Coq
33:CoC
19:In
2896::
2812:.
2732:76
2730:.
2724:.
2713:;
2684:.
2666:.
1836::=
1746:.
1615:.
1505:.
1437:.
1388:.
1233:.
1152::=
1027:;
704::
210:);
177:A
141:.
115:.
65:.
2846:.
2820:.
2802:.
2800:B
2786:B
2783:.
2780:A
2777::
2774:x
2744:.
2738::
2694:.
2652:.
2565:B
2559:A
2538:B
2535:+
2532:A
2510:B
2504:A
2483:B
2477:A
2455:A
2449:A
2443:)
2440:A
2434:A
2431:(
2428:.
2424:P
2420::
2417:A
2390:A
2384:A
2378:A
2375:.
2371:P
2367::
2364:A
2322:C
2316:)
2313:)
2310:C
2304:B
2301:(
2298:.
2295:A
2292::
2289:x
2283:(
2280:.
2276:P
2272::
2269:C
2256:B
2253:.
2250:A
2247::
2244:x
2233:)
2230:C
2224:A
2221:(
2218:.
2214:P
2210::
2207:C
2194:A
2183:C
2177:)
2174:C
2168:B
2165:(
2159:)
2156:C
2150:A
2147:(
2144:.
2140:P
2136::
2133:C
2120:B
2114:A
2106:C
2100:)
2097:C
2091:B
2085:A
2082:(
2079:.
2075:P
2071::
2068:C
2055:B
2049:A
2042:)
2039:B
2033:x
2030:(
2025:B
2022:.
2019:A
2016::
2013:x
2000:B
1994:A
1937:B
1934::
1931:M
1920:K
1917::
1914:B
1903:B
1894:=
1890:A
1885:A
1882::
1879:M
1860:6
1842:]
1839:N
1833:x
1830:[
1827:B
1824::
1821:N
1818:M
1807:A
1804::
1801:N
1790:)
1787:B
1784:.
1781:A
1778::
1775:x
1769:(
1766::
1763:M
1744:5
1726:)
1723:B
1720:.
1717:A
1714::
1711:x
1705:(
1702::
1699:)
1696:N
1693:.
1690:A
1687::
1684:x
1678:(
1667:B
1664::
1661:N
1655:A
1652::
1649:x
1646:,
1638:K
1635::
1632:A
1613:4
1595:L
1592::
1589:)
1586:B
1583:.
1580:A
1577::
1574:x
1568:(
1557:L
1554::
1551:B
1545:A
1542::
1539:x
1536:,
1528:K
1525::
1522:A
1503:3
1485:A
1482::
1479:x
1465:,
1462:A
1459::
1456:x
1453:,
1435:2
1416:T
1412::
1408:P
1386:1
1376:.
1364:D
1361::
1358:C
1327:B
1324::
1321:A
1299:,
1284:D
1281::
1278:C
1262:B
1259::
1256:A
1221:B
1201:x
1178:N
1158:]
1155:N
1149:x
1146:[
1143:B
1122:T
1100:P
1079:L
1076:,
1073:K
1053:D
1050:,
1047:C
1044:,
1041:B
1038:,
1035:A
1012:,
1007:2
1003:A
999::
994:2
990:x
986:,
981:1
977:A
973::
968:1
964:x
931:.
919:B
899:t
876:,
871:2
867:A
863:,
858:1
854:A
830:,
825:2
821:x
817:,
812:1
808:x
791:,
779:B
776::
773:t
764:,
759:2
755:A
751::
746:2
742:x
738:,
733:1
729:A
725::
720:1
716:x
678:T
654:P
633:;
623:;
597:e
594:.
591:e
586::
581:x
572:e
569:.
566:e
561::
556:x
547:e
543:e
537:x
530:P
522:T
515:e
494:.
482:)
479:B
476:.
473:A
470::
467:x
461:(
451:,
439:)
436:B
433:.
430:A
427::
424:x
418:(
396:x
376:B
356:A
345:;
333:)
330:B
327:A
324:(
304:B
284:A
258:,
255:y
252:,
249:x
221:P
193:T
31:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.