git @ Cat's Eye Technologies The-Glosscubator / 37bb8c2
Split Coq off from Theorem Proving. Chris Pressey 1 year, 1 month ago
6 changed file(s) with 87 addition(s) and 44 deletion(s). Raw diff Collapse all Expand all
+12
-0
Coq/Books.md less more
0 Coq Books
1 =========
2
3 ### Software Foundations
4
5 * authors: Benjamin C. Pierce et al
6 * date: 2024
7 * online @ [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/)
8
9 So this is actually a collection of several volumns. Should I split it up? Not sure.
10
11 As of 2024 the first volume is at version 6.6. I don't know when this started.
+35
-0
Coq/README.md less more
0 Coq
1 ---
2
3 <!--
4 SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
5
6 SPDX-License-Identifier: CC0-1.0
7 -->
8 _See also: [Theorem Proving](../Theorem%20Proving/)_
9
10 - - - -
11
12 ### Coq
13
14 [implication - Transitivity of -\> in Coq - Stack Overflow](https://stackoverflow.com/questions/55295029/transitivity-of-in-coq)
15
16 [proof - Proving (\~A -\> \~B)-\> (\~A -\> B) -\> A in Coq - Stack Overflow](https://stackoverflow.com/questions/55232025/proving-a-b-a-b-a-in-coq)
17
18 [coq - Proving f (f bool) = bool - Stack Overflow](https://stackoverflow.com/questions/1674018/proving-f-f-bool-bool)
19
20 [Address a \"setoid hell\"? · Issue \#10871 · coq/coq](https://github.com/coq/coq/issues/10871)
21
22 ### Calculus of [Inductive] Constructions
23
24 [Calculus of constructions - Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions)
25
26 [Introduction to the Calculus of Inductive Constructions - Christine Paulin-Mohring (pdf)](https://inria.hal.science/hal-01094195/document)
27
28 [The Calculus of Inductive Constructions - Hugo Herbelin (pdf)](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf)
29
30 [lo.logic - Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic - Theoretical Computer Science Stack Exchange](https://cstheory.stackexchange.com/questions/53656/intuitive-explanation-of-the-fact-that-the-calculus-of-constructions-is-not-cons)
31
32 ### Books
33
34 Software Foundations (online @ [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/))
+30
-0
Coq/Webpages.md less more
0 Coq
1 ---
2
3 <!--
4 SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
5
6 SPDX-License-Identifier: CC0-1.0
7 -->
8
9 - - - -
10
11 ### Coq
12
13 [implication - Transitivity of -\> in Coq - Stack Overflow](https://stackoverflow.com/questions/55295029/transitivity-of-in-coq)
14
15 [proof - Proving (\~A -\> \~B)-\> (\~A -\> B) -\> A in Coq - Stack Overflow](https://stackoverflow.com/questions/55232025/proving-a-b-a-b-a-in-coq)
16
17 [coq - Proving f (f bool) = bool - Stack Overflow](https://stackoverflow.com/questions/1674018/proving-f-f-bool-bool)
18
19 [Address a \"setoid hell\"? · Issue \#10871 · coq/coq](https://github.com/coq/coq/issues/10871)
20
21 ### Calculus of [Inductive] Constructions
22
23 [Calculus of constructions - Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions)
24
25 [Introduction to the Calculus of Inductive Constructions - Christine Paulin-Mohring (pdf)](https://inria.hal.science/hal-01094195/document)
26
27 [The Calculus of Inductive Constructions - Hugo Herbelin (pdf)](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf)
28
29 [lo.logic - Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic - Theoretical Computer Science Stack Exchange](https://cstheory.stackexchange.com/questions/53656/intuitive-explanation-of-the-fact-that-the-calculus-of-constructions-is-not-cons)
+9
-0
TOPICS.md less more
147147
148148 Placeholder description.
149149
150 ### Coq
151
152 * used-in: bookmarks
153 * see-also: Theorem Proving
154
155 Works regarding the proof assistant Coq, its language Gallina, and
156 its underlying theory, the Calculus of [Inductive] Constructions.
157
150158 ### Database Theory
151159
152160 * used-in: books
590598 ### Theorem Proving
591599
592600 * used-in: books, bookmarks
601 * see-also: Specification, Coq
593602
594603 Placeholder description.
595604
+1
-22
Theorem Proving/README.md less more
55
66 SPDX-License-Identifier: CC0-1.0
77 -->
8 _See also: [Specification](../Specification/), [Coq](../Coq/)_
89
910 - - - -
1011
3637
3738 [HOL88/src/ml/hol-rule.ml at master · theoremprover-museum/HOL88](https://github.com/theoremprover-museum/HOL88/blob/master/src/ml/hol-rule.ml)
3839
39 ### Coq (and CoC, and CIC)
40
41 [Software Foundations](https://softwarefoundations.cis.upenn.edu/)
42
43 [Logical Foundations - Table of contents](https://softwarefoundations.cis.upenn.edu/lf-current/toc.html)
44
45 [implication - Transitivity of -\> in Coq - Stack Overflow](https://stackoverflow.com/questions/55295029/transitivity-of-in-coq)
46
47 [proof - Proving (\~A -\> \~B)-\> (\~A -\> B) -\> A in Coq - Stack Overflow](https://stackoverflow.com/questions/55232025/proving-a-b-a-b-a-in-coq)
48
49 [coq - Proving f (f bool) = bool - Stack Overflow](https://stackoverflow.com/questions/1674018/proving-f-f-bool-bool)
50
51 [Calculus of constructions - Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions)
52
53 [Introduction to the Calculus of Inductive Constructions - Christine Paulin-Mohring (pdf)](https://inria.hal.science/hal-01094195/document)
54
55 [The Calculus of Inductive Constructions - Hugo Herbelin (pdf)](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf)
56
57 [lo.logic - Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic - Theoretical Computer Science Stack Exchange](https://cstheory.stackexchange.com/questions/53656/intuitive-explanation-of-the-fact-that-the-calculus-of-constructions-is-not-cons)
58
59 [Address a \"setoid hell\"? · Issue \#10871 · coq/coq](https://github.com/coq/coq/issues/10871)
60
6140 ### Lean
6241
6342 [Theorem Proving in Lean 4 - Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/)
+0
-22
Theorem Proving/Webpages.md less more
3636
3737 [HOL88/src/ml/hol-rule.ml at master · theoremprover-museum/HOL88](https://github.com/theoremprover-museum/HOL88/blob/master/src/ml/hol-rule.ml)
3838
39 ### Coq (and CoC, and CIC)
40
41 [Software Foundations](https://softwarefoundations.cis.upenn.edu/)
42
43 [Logical Foundations - Table of contents](https://softwarefoundations.cis.upenn.edu/lf-current/toc.html)
44
45 [implication - Transitivity of -\> in Coq - Stack Overflow](https://stackoverflow.com/questions/55295029/transitivity-of-in-coq)
46
47 [proof - Proving (\~A -\> \~B)-\> (\~A -\> B) -\> A in Coq - Stack Overflow](https://stackoverflow.com/questions/55232025/proving-a-b-a-b-a-in-coq)
48
49 [coq - Proving f (f bool) = bool - Stack Overflow](https://stackoverflow.com/questions/1674018/proving-f-f-bool-bool)
50
51 [Calculus of constructions - Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions)
52
53 [Introduction to the Calculus of Inductive Constructions - Christine Paulin-Mohring (pdf)](https://inria.hal.science/hal-01094195/document)
54
55 [The Calculus of Inductive Constructions - Hugo Herbelin (pdf)](https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf)
56
57 [lo.logic - Intuitive explanation of the fact that the Calculus of Constructions is not conservative over Higher-Order Logic - Theoretical Computer Science Stack Exchange](https://cstheory.stackexchange.com/questions/53656/intuitive-explanation-of-the-fact-that-the-calculus-of-constructions-is-not-cons)
58
59 [Address a \"setoid hell\"? · Issue \#10871 · coq/coq](https://github.com/coq/coq/issues/10871)
60
6139 ### Lean
6240
6341 [Theorem Proving in Lean 4 - Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4/)