git @ Cat's Eye Technologies The-Glosscubator / e3dfd88
More automation, more extraction of ratings. Chris Pressey 1 year, 28 days ago
26 changed file(s) with 714 addition(s) and 105 deletion(s). Raw diff Collapse all Expand all
1212 * authors: Ian Stewart
1313 * date: 1998
1414 * borrow @ [archive.org](https://archive.org/details/magicalmazeseein0000stew)
15 * rating: 3
1615
1716 An entertaining philosophical introduction to mathematics; pop-sci, but not irritatingly so.
1817
2221 * author: Paul Hoffman
2322 * date: 1988
2423 * borrow @ [archive.org](https://archive.org/details/archimedesreveng00hoff_0)
25 * rating: 1
2624
2725 .
2826
1212 * date: 2015
1313 * publication: arXiv.org
1414 * online @ [arxiv.org](https://arxiv.org/abs/1506.06319)
15 * rating: 3
1615
1716 .
1515 ### Examples of common false beliefs in mathematics. - MathOverflow
1616
1717 * url: http://mathoverflow.net/questions/23478/examples-of-common-false-beliefs-in-mathematics
18 * rating: 1
1918
2019 .
2120
2221 ### soft question - Math papers where the only issue is that someone else could\'ve done it but didn\'t - MathOverflow
2322
2423 * url: https://mathoverflow.net/questions/433686/math-papers-where-the-only-issue-is-that-someone-else-couldve-done-it-but-didn
25 * rating: 1
2624
2725 .
2826
2927 ### soft question - When has the scaffolding been more important than the completed building? - MathOverflow
3028
3129 * url: https://mathoverflow.net/questions/459252/when-has-the-scaffolding-been-more-important-than-the-completed-building
32 * rating: 1
3330
3431 .
3532
3633 ### soft question - Big ideas that began small or small ideas that became big - MathOverflow
3734
3835 * url: https://mathoverflow.net/questions/369179/big-ideas-that-began-small-or-small-ideas-that-became-big
39 * rating: 1
4036
4137 .
4238
4339 ### reference request - Proofs of theorems that proved more or deeper results than what was first supposed or stated as the corresponding theorem - MathOverflow
4440
4541 * url: https://mathoverflow.net/questions/385732/proofs-of-theorems-that-proved-more-or-deeper-results-than-what-was-first-suppos
46 * rating: 1
4742
4843 .
4944
5045 ### big list - Every mathematician has only a few tricks - MathOverflow
5146
5247 * url: https://mathoverflow.net/questions/363119/every-mathematician-has-only-a-few-tricks
53 * rating: 1
5448
5549 .
5650
5751 ### Poincaré on intuition in mathematics - MacTutor History of Mathematics
5852
5953 * url: https://mathshistory.st-andrews.ac.uk/Extras/Poincare_Intuition/
60 * rating: classic
6154
6255 .
6356
6457 ### There's more to mathematics than rigour and proofs \| What\'s new
6558
6659 * url: https://terrytao.wordpress.com/career-advice/theres-more-to-mathematics-than-rigour-and-proofs/
67 * rating: 1
6860
6961 .
7062
7163 ### soft question - Is an interpretation mathematics (fit for publication)? - MathOverflow
7264
7365 * url: https://mathoverflow.net/questions/386789/is-an-interpretation-mathematics-fit-for-publication
74 * rating: 1
7566
7667 .
7768
7869 ### mathematics education - Are hypergeometric series not taught often at universities nowadays, and if so, why? - MathOverflow
7970
8071 * url: https://mathoverflow.net/questions/391124/are-hypergeometric-series-not-taught-often-at-universities-nowadays-and-if-so
81 * rating: 1
8272
8373 .
8474
8575 ### calculus - Is there a reason it is so rare we can solve differential equations? - Mathematics Stack Exchange
8676
8777 * url: https://math.stackexchange.com/questions/3782499/is-there-a-reason-it-is-so-rare-we-can-solve-differential-equations
88 * rating: 1
8978
9079 .
9180
9281 ### logic - How many words (i.e. not \"math\" symbols\") should I use in my proofs? - Mathematics Stack Exchange
9382
9483 * url: https://math.stackexchange.com/questions/2701182/how-many-words-i-e-not-math-symbols-should-i-use-in-my-proofs
95 * rating: 1
9684
9785 .
9886
9987 ### fa.functional analysis - Why do we have two theorems when one implies the other? - MathOverflow
10088
10189 * url: https://mathoverflow.net/questions/397286/why-do-we-have-two-theorems-when-one-implies-the-other
102 * rating: 1
10390
10491 .
10592
10693 ### soft question - Theorems with many distinct proofs - MathOverflow
10794
10895 * url: https://mathoverflow.net/questions/401493/theorems-with-many-distinct-proofs/401519
109 * rating: 1
11096
11197 .
11298
11399 ### \"Strange\" proofs of existence theorems - MathOverflow
114100
115101 * url: https://mathoverflow.net/questions/312439/strange-proofs-of-existence-theorems
116 * rating: 1
117102
118103 .
119104
126111 ### mathematical pedagogy - Why\'s math way more puzzling, abstruse than law and medicine? - Mathematics Educators Stack Exchange
127112
128113 * url: https://matheducators.stackexchange.com/questions/24706/whys-math-way-more-puzzling-abstruse-than-law-and-medicine
129 * rating: 1
130114
131115 .
132116
133117 ### Why there is no Hitchhiker's Guide to Mathematics for Programmers \| Math ∩ Programming
134118
135119 * url: http://jeremykun.com/2013/02/08/why-there-is-no-hitchhikers-guide-to-mathematics-for-programmers/#comment-1345
136 * rating: 1
137120
138121 .
139122
140123 ### mathematics - How can I counter a student response saying \"Why are we bothered to reinvent the wheel when proving mathematical identities?\" - Academia Stack Exchange
141124
142125 * url: https://academia.stackexchange.com/questions/155433/how-can-i-counter-a-student-response-saying-why-are-we-bothered-to-reinvent-the
143 * rating: 1
144126
145127 .
146128
147129 ### secondary education - Response to Students Who Say \"This Is Not Important\" - Mathematics Educators Stack Exchange
148130
149131 * url: https://matheducators.stackexchange.com/questions/20962/response-to-students-who-say-this-is-not-important
150 * rating: 1
151132
152133 .
153134
154135 ### soft question - Daunting papers/books and how to finally read them - MathOverflow
155136
156137 * url: https://mathoverflow.net/questions/463287/daunting-papers-books-and-how-to-finally-read-them
157 * rating: 1
158138
159139 .
160140
161141 ### books - Learning mathematics in an \"independent and idiosyncratic\" way - MathOverflow
162142
163143 * url: https://mathoverflow.net/questions/371038/learning-mathematics-in-an-independent-and-idiosyncratic-way
164 * rating: 1
165144
166145 .
167146
174153 ### Why is writing down mathematical proofs more fault-proof than writing computer code? - Computer Science Stack Exchange
175154
176155 * url: https://cs.stackexchange.com/questions/85327/why-is-writing-down-mathematical-proofs-more-fault-proof-than-writing-computer-c
177 * rating: 1
178156
179157 .
180158
181159 ### soft question - Consequences of lack of rigour - MathOverflow
182160
183161 * url: https://mathoverflow.net/questions/324257/consequences-of-lack-of-rigour
184 * rating: 1
185162
186163 .
187164
188165 ### history - Soft question: Examples where lack of mathematical rigour cause security breaches? - Cryptography Stack Exchange
189166
190167 * url: https://crypto.stackexchange.com/questions/71024/soft-question-examples-where-lack-of-mathematical-rigour-cause-security-breache)
191 * rating: 1
192168
193169 .
194170
201177 ### research - Replication crisis in mathematics - MathOverflow
202178
203179 * url: https://mathoverflow.net/questions/370898/replication-crisis-in-mathematics
204 * rating: 1
205180
206181 .
207182
208183 ### Titans of Mathematics Clash Over Epic Proof of ABC Conjecture \| Quanta Magazine
209184
210185 * url: https://www.quantamagazine.org/titans-of-mathematics-clash-over-epic-proof-of-abc-conjecture-20180920/
211 * rating: 1
212186
213187 .
214188
215189 ### The ABC conjecture has (still) not been proved \| Persiflage
216190
217191 * url: https://www.galoisrepresentations.com/2017/12/17/the-abc-conjecture-has-still-not-been-proved/
218 * rating: 1
219192
220193 .
221194
222195 ### Notes on the Oxford IUT workshop by Brian Conrad \| mathbabe
223196
224197 * url: https://mathbabe.org/2015/12/15/notes-on-the-oxford-iut-workshop-by-brian-conrad/
225 * rating: 1
226198
227199 .
228200
229201 ### ho.history overview - Endless controversy - MathOverflow
230202
231203 * url: https://mathoverflow.net/questions/282742/endless-controversy
232 * rating: 1
233204
234205 .
235206
236207 ### independent researcher - Why are most cranks old men? - Academia Stack Exchange
237208
238209 * url: https://academia.stackexchange.com/questions/145242/why-are-most-cranks-old-men
239 * rating: 1
240210
241211 .
242212
267237 ### abstract algebra - Can we define algebraic structures (group, rings, modules, fields) via their arrows? - Mathematics Stack Exchange
268238
269239 * url: https://math.stackexchange.com/questions/3586965/can-we-define-algebraic-structures-group-rings-modules-fields-via-their-arr#3588120
270 * rating: 1
271240
272241 .
273242
274243 ### algebra precalculus - If two pairs of numbers have equal sums and products, what can we conclude about the pairs? - Mathematics Stack Exchange
275244
276245 * url: https://math.stackexchange.com/questions/4825276/if-two-pairs-of-numbers-have-equal-sums-and-products-what-can-we-conclude-about
277 * rating: 1
278246
279247 .
280248
281249 ### Readings | Mathematics for Computer Science | Electrical Engineering and Computer Science | MIT OpenCourseWare
282250
283251 * url: https://ocw.mit.edu/courses/6-042j-mathematics-for-computer-science-fall-2010/pages/readings/
284 * rating: 2
285252 * topics: Mathematics, Logic, Probability Theory
286253
287254 collection of course notes PDFs.
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Mathematics
13 ---------------
14
15 ### The Magical Maze
16
17 * rating: 3
18
19 .
20
21 ### Archimedes' Revenge
22
23 * rating: 1
24
25 .
26
27 ### Compactness and Contradiction
28
29 * rating: TODO
30
31 .
32
33 ### Infinity - A simple, but not too simple introduction
34
35 * rating: 3
36
37 .
38
39 ### Practice of mathematics
40
41 * rating: TODO
42
43 .
44
45 ### Examples of common false beliefs in mathematics. - MathOverflow
46
47 * rating: 1
48
49 .
50
51 ### soft question - Math papers where the only issue is that someone else could\'ve done it but didn\'t - MathOverflow
52
53 * rating: 1
54
55 .
56
57 ### soft question - When has the scaffolding been more important than the completed building? - MathOverflow
58
59 * rating: 1
60
61 .
62
63 ### soft question - Big ideas that began small or small ideas that became big - MathOverflow
64
65 * rating: 1
66
67 .
68
69 ### reference request - Proofs of theorems that proved more or deeper results than what was first supposed or stated as the corresponding theorem - MathOverflow
70
71 * rating: 1
72
73 .
74
75 ### big list - Every mathematician has only a few tricks - MathOverflow
76
77 * rating: 1
78
79 .
80
81 ### Poincaré on intuition in mathematics - MacTutor History of Mathematics
82
83 * rating: classic
84
85 .
86
87 ### There's more to mathematics than rigour and proofs \| What\'s new
88
89 * rating: 1
90
91 .
92
93 ### soft question - Is an interpretation mathematics (fit for publication)? - MathOverflow
94
95 * rating: 1
96
97 .
98
99 ### mathematics education - Are hypergeometric series not taught often at universities nowadays, and if so, why? - MathOverflow
100
101 * rating: 1
102
103 .
104
105 ### calculus - Is there a reason it is so rare we can solve differential equations? - Mathematics Stack Exchange
106
107 * rating: 1
108
109 .
110
111 ### logic - How many words (i.e. not \"math\" symbols\") should I use in my proofs? - Mathematics Stack Exchange
112
113 * rating: 1
114
115 .
116
117 ### fa.functional analysis - Why do we have two theorems when one implies the other? - MathOverflow
118
119 * rating: 1
120
121 .
122
123 ### soft question - Theorems with many distinct proofs - MathOverflow
124
125 * rating: 1
126
127 .
128
129 ### \"Strange\" proofs of existence theorems - MathOverflow
130
131 * rating: 1
132
133 .
134
135 ### Studying mathematics
136
137 * rating: TODO
138
139 .
140
141 ### mathematical pedagogy - Why\'s math way more puzzling, abstruse than law and medicine? - Mathematics Educators Stack Exchange
142
143 * rating: 1
144
145 .
146
147 ### Why there is no Hitchhiker's Guide to Mathematics for Programmers \| Math ∩ Programming
148
149 * rating: 1
150
151 .
152
153 ### mathematics - How can I counter a student response saying \"Why are we bothered to reinvent the wheel when proving mathematical identities?\" - Academia Stack Exchange
154
155 * rating: 1
156
157 .
158
159 ### secondary education - Response to Students Who Say \"This Is Not Important\" - Mathematics Educators Stack Exchange
160
161 * rating: 1
162
163 .
164
165 ### soft question - Daunting papers/books and how to finally read them - MathOverflow
166
167 * rating: 1
168
169 .
170
171 ### books - Learning mathematics in an \"independent and idiosyncratic\" way - MathOverflow
172
173 * rating: 1
174
175 .
176
177 ### Mathematical Rigour
178
179 * rating: TODO
180
181 .
182
183 ### Why is writing down mathematical proofs more fault-proof than writing computer code? - Computer Science Stack Exchange
184
185 * rating: 1
186
187 .
188
189 ### soft question - Consequences of lack of rigour - MathOverflow
190
191 * rating: 1
192
193 .
194
195 ### history - Soft question: Examples where lack of mathematical rigour cause security breaches? - Cryptography Stack Exchange
196
197 * rating: 1
198
199 .
200
201 ### Controversy in mathematics
202
203 * rating: TODO
204
205 .
206
207 ### research - Replication crisis in mathematics - MathOverflow
208
209 * rating: 1
210
211 .
212
213 ### Titans of Mathematics Clash Over Epic Proof of ABC Conjecture \| Quanta Magazine
214
215 * rating: 1
216
217 .
218
219 ### The ABC conjecture has (still) not been proved \| Persiflage
220
221 * rating: 1
222
223 .
224
225 ### Notes on the Oxford IUT workshop by Brian Conrad \| mathbabe
226
227 * rating: 1
228
229 .
230
231 ### ho.history overview - Endless controversy - MathOverflow
232
233 * rating: 1
234
235 .
236
237 ### independent researcher - Why are most cranks old men? - Academia Stack Exchange
238
239 * rating: 1
240
241 .
242
243 ### People
244
245 * rating: TODO
246
247 .
248
249 ### Paul du Bois-Reymond - Wikipedia
250
251 * rating: TODO
252
253 .
254
255 ### James Dugundji - Wikipedia
256
257 * rating: TODO
258
259 .
260
261 ### Other
262
263 * rating: TODO
264
265 .
266
267 ### abstract algebra - Can we define algebraic structures (group, rings, modules, fields) via their arrows? - Mathematics Stack Exchange
268
269 * rating: 1
270
271 .
272
273 ### algebra precalculus - If two pairs of numbers have equal sums and products, what can we conclude about the pairs? - Mathematics Stack Exchange
274
275 * rating: 1
276
277 .
278
279 ### Readings | Mathematics for Computer Science | Electrical Engineering and Computer Science | MIT OpenCourseWare
280
281 * rating: 2
282
283 .
284
99 ### Counterexamples in Type Systems
1010
1111 * online @ [counterexamples.org](https://counterexamples.org/)
12 * rating: 2
1312
1413 .
1313 * publication: ACM Transactions on Programming Languages and Systems
1414 * online @ [lamport.azurewebsites.net](http://lamport.azurewebsites.net/pubs/lamport-types.pdf) (PDF)
1515 * topics: Specification, Type Systems
16 * rating: 3
1716
1817 .
1918
2322 * date: 2009
2423 * publication: OOPSLA '09: Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications
2524 * online @ [cs.utexas.edu](https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf) (PDF)
26 * rating: 3
2725
2826 .
2927
3331 * date: 2014
3432 * publication: Onward!
3533 * online @ [kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/srk21/papers/kell14in-author-version.pdf) (PDF)
36 * rating: 3
3734
3835 .
3936
4239 * authors: Simone Martini
4340 * date: 2016
4441 * online @ [arxiv.org](https://arxiv.org/abs/1510.03726)
45 * rating: TODO
4642
4743 .
4844
5147 * authors: Jeremy Gibbons
5248 * online @ [www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf)
5349 * date: 2008
54 * rating: 3
5550
5651 .
5752
6156 * date: 2007
6257 * online @ [libres.uncg.edu](https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2007_Intitial%20Algebra%20Semantics%20Is%20Enough.pdf)
6358 * topics: Type Systems, Functional Programming
64 * rating: TODO
6559
6660 .
6761
7064 * authors: Flemming Nielson, Hanne Riis Nielson
7165 * date: 1999
7266 * online @ [web.cs.ucla.edu](https://web.cs.ucla.edu/~palsberg/tba/papers/nielson-nielson-csd99.pdf)
73 * rating: 1
7467
7568 .
7669
8073 * date: 1988
8174 * online @ [homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf)
8275 * topics: Type Systems, Type Theory
83 * rating: TODO
8476
8577 .
99 ### type safety - What is the difference between a strongly typed language and a statically typed language? - Stack Overflow
1010
1111 * url: https://stackoverflow.com/questions/2690544/what-is-the-difference-between-a-strongly-typed-language-and-a-statically-typed#2696369
12 * rating: 3
1312
1413 .
1514
1615 ### What is a strictly typed language? - Stack Overflow
1716
1817 * url: https://stackoverflow.com/questions/805168/what-is-a-strictly-typed-language
19 * rating: 1
2018
2119 .
2220
2321 ### Coeffects: The next big programming challenge - Tomas Petricek
2422
2523 * url: http://tomasp.net/blog/2014/why-coeffects-matter/
26 * rating: 1
2724
2825 .
2926
3027 ### Type Constraints · The Programming Languages Laboratory
3128
3229 * url: https://www.pl.cs.jhu.edu/projects/type-constraints/
33 * rating: 1
3430
3531 collection of papers from an (inactive) research project
3632
3733 ### The algebra (and calculus!) of algebraic data types
3834
3935 * url: https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types
40 * rating: 3
4136 * topics: Type Systems, Type Theory, Mathematics
4237
4338 future-topics: Abstract Algebra
4540 ### What is a type and effect system? - Stack Overflow
4641
4742 * url: https://stackoverflow.com/questions/196465/what-is-a-type-and-effect-system
48 * rating: 1
4943
5044 .
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Type Systems
13 ---------------
14
15 ### Counterexamples in Type Systems
16
17 * rating: 2
18
19 .
20
21 ### Should Your Specification Language Be Typed?
22
23 * rating: 3
24
25 .
26
27 ### On Understanding Data Abstraction, Revisited
28
29 * rating: 3
30
31 .
32
33 ### In Search of Types
34
35 * rating: 3
36
37 .
38
39 ### Several types of types in programming languages
40
41 * rating: TODO
42
43 .
44
45 ### Unfolding Abstract Datatypes
46
47 * rating: 3
48
49 .
50
51 ### Initial Algebra Semantics is Enough!
52
53 * rating: TODO
54
55 .
56
57 ### Type and Effect Systems
58
59 * rating: 1
60
61 .
62
63 ### Abstract Types have Existential Type
64
65 * rating: TODO
66
67 .
68
69 ### type safety - What is the difference between a strongly typed language and a statically typed language? - Stack Overflow
70
71 * rating: 3
72
73 .
74
75 ### What is a strictly typed language? - Stack Overflow
76
77 * rating: 1
78
79 .
80
81 ### Coeffects: The next big programming challenge - Tomas Petricek
82
83 * rating: 1
84
85 .
86
87 ### Type Constraints · The Programming Languages Laboratory
88
89 * rating: 1
90
91 .
92
93 ### The algebra (and calculus!) of algebraic data types
94
95 * rating: 3
96
97 .
98
99 ### What is a type and effect system? - Stack Overflow
100
101 * rating: 1
102
103 .
104
1111 * author: Roger Hindley
1212 * date: 1997
1313 * borrow @ [archive.org](https://archive.org/details/basicsimpletypet0000hind)
14 * rating: TODO
1514
16 When I first tried to read it, I found it neither basic nor simple.
15 .
1716
1817 ### Type Theory and Functional Programming
1918
2120 * date: 1999
2221 * online @ [www.cs.kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf)
2322 * topics: Type Theory, Functional Programming
24 * rating: TODO
2523
26 I need to try to read this in earnest someday.
24 .
2725
2826 ### Programming in Martin-Löf’s Type Theory
2927
3129 * authors: Bengt Nordström, Kent Petersson, Jan M. Smith
3230 * date: 1990
3331 * online @ [www.cse.chalmers.se](http://www.cse.chalmers.se/research/group/logic/book/)
34 * rating: TODO
3532
3633 .
3734
99 ### The Gentle Art of Levitation (pdf)
1010
1111 * url: https://personal.cis.strath.ac.uk/conor.mcbride/levitation.pdf
12 * rating: TODO
1312
1413 .
1514
1615 ### Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
1716
1817 * url: https://web.archive.org/web/20211207042011/http://compilers.cs.ucla.edu/popl16/
19 * rating: TODO
2018
2119 .
2220
2523 * authors: Arie Middelkoop, Atze Dijkstra, S. Doaitse Swierstra
2624 * date: 2011
2725 * online @ [link.springer.com](https://link.springer.com/article/10.1007/s10990-011-9065-0)
28 * rating: TODO
2926
3027 .
99 ### Type Theory (Stanford Encyclopedia of Philosophy)
1010
1111 * url: https://plato.stanford.edu/entries/type-theory/
12 * rating: 2
1312
14 future-rating: 2.5
13 .
1514
1615 ### Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy)
1716
1817 * url: https://plato.stanford.edu/entries/type-theory-intuitionistic/
19 * rating: 2
2018
21 future-rating: 2.5
19 .
2220
2321 ### computability - Does there exist a Turing complete typed lambda calculus? - Computer Science Stack Exchange
2422
2523 * url: https://cs.stackexchange.com/questions/2638/does-there-exist-a-turing-complete-typed-lambda-calculus
26 * rating: 1
2724
2825 .
2926
3027 ### Characterization of lambda-terms that have union types - Computer Science Stack Exchange
3128
3229 * url: https://cs.stackexchange.com/questions/62/characterization-of-lambda-terms-that-have-union-types/88#88
33 * rating: 1
3430
3531 .
3632
3733 ### Type Theory and Mathematical Logic \| artagnon.com
3834
3935 * url: https://artagnon.com/logic
40 * rating: 1
4136 * topics: Type Theory, FoM, Logic
4237
4338 .
4540 ### Typed Combinators
4641
4742 * url: http://chriswarbo.net/blog/2012-12-01-typed_combinators.html
48 * rating: 1
4943
5044 .
5145
5347
5448 * url: https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
5549 * topics: Type Theory, Category Theory
56 * rating: 1
5750
5851 .
5952
6053 ### Computational type theory - Scholarpedia
6154
6255 * url: http://www.scholarpedia.org/article/Computational_type_theory
63 * rating: 0
6456
6557 .
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Type Theory
13 ---------------
14
15 ### Basic Simple Type Theory
16
17 * rating: TODO
18
19 When I first tried to read it, I found it neither basic nor simple.
20
21 ### Type Theory and Functional Programming
22
23 * rating: TODO
24
25 .
26
27 ### Programming in Martin-Löf’s Type Theory
28
29 * rating: TODO
30
31 .
32
33 ### The Gentle Art of Levitation (pdf)
34
35 * rating: TODO
36
37 .
38
39 ### Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
40
41 * rating: TODO
42
43 .
44
45 ### A lean specification for GADTs: system F with first-class equality proofs
46
47 * rating: TODO
48
49 .
50
51 ### Type Theory (Stanford Encyclopedia of Philosophy)
52
53 * rating: 2
54
55 future-rating: 2.5
56
57 ### Intuitionistic Type Theory (Stanford Encyclopedia of Philosophy)
58
59 * rating: 2
60
61 future-rating: 2.5
62
63 ### computability - Does there exist a Turing complete typed lambda calculus? - Computer Science Stack Exchange
64
65 * rating: 1
66
67 .
68
69 ### Characterization of lambda-terms that have union types - Computer Science Stack Exchange
70
71 * rating: 1
72
73 .
74
75 ### Type Theory and Mathematical Logic \| artagnon.com
76
77 * rating: 1
78
79 .
80
81 ### Typed Combinators
82
83 * rating: 1
84
85 .
86
87 ### Recursive Types for Free! (Philip Wadler)
88
89 * rating: 1
90
91 .
92
93 ### Computational type theory - Scholarpedia
94
95 * rating: 0
96
97 .
98
1111 * authors: Kevin Knight
1212 * date: 1989
1313 * online @ [kevincrawfordknight.github.io](https://kevincrawfordknight.github.io/papers/unification-knight.pdf)
14 * rating: 1
1514
1615 .
1716
2019 * authors: Peter Norvig
2120 * date: 1990???
2221 * online @ [norvig.com](https://norvig.com/unify-bug.pdf)
23 * rating: 1
2422
2523 .
1111 * url: https://github.com/mrocklin/unification
1212 * license: BSD-3-Clause
1313 * topics: Unification, Python
14 * rating: 1
1514
1615 .
1716
2019 * url: https://github.com/parsonsmatt/unification
2120 * license: BSD-3-Clause
2221 * topics: Unification, Haskell
23 * rating: 1
2422
2523 .
2624
2927 * url: https://github.com/jozefg/higher-order-unification
3028 * license: MIT
3129 * topics: Unification, Haskell
32 * rating: 1
3330
3431 .
99 ### Notes: Unification
1010
1111 * url: http://www.cs.trincoll.edu/~ram/cpsc352/notes/unification.html
12 * rating: 1
1312
1413 .
1514
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 Unification
13 ---------------
14
15 ### Unification: A Multidisciplinary Survey
16
17 * rating: 1
18
19 .
20
21 ### Correcting a Widespread Error in Unification Algorithms
22
23 * rating: 1
24
25 .
26
27 ### Notes: Unification
28
29 * rating: 1
30
31 .
32
33 ### mrocklin/unification
34
35 * rating: 1
36
37 .
38
39 ### parsonsmatt/unification: implementation of the first order logic unification algorithm in Haskell
40
41 * rating: 1
42
43 .
44
45 ### jozefg/higher-order-unification: A small implementation of higher-order unification
46
47 * rating: 1
48
49 .
50
1111 * author: Jef Raskin
1212 * date: 2000
1313 * borrow @ [archive.org](https://archive.org/details/humaneinterfacen00rask)
14 * rating: 2
1514
1615 .
1716
2019 * author: Ian Horrocks
2120 * date: 1999
2221 * borrow @ [archive.org](https://archive.org/details/isbn_9780201342789)
23 * rating: 1
2422
2523 .
1010
1111 * url: https://github.com/akalenuk/16counters
1212 * license: Unlicense
13 * rating: 3
1413
1514 .
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 User Interface
13 ---------------
14
15 ### The Humane Interface
16
17 * rating: 2
18
19 .
20
21 ### Constructing the User Interface with Statecharts
22
23 * rating: 1
24
25 .
26
27 ### akalenuk/16counters: GUI for those who don't do GUI
28
29 * rating: 3
30
31 .
32
1010
1111 * authors: Daniel P. Friedman, William E. Byrd, Oleg Kiselyov
1212 * borrow @ [archive.org](https://archive.org/details/reasonedschemer0000frie)
13 * rating: 1
1413
1514 It is written in "programed" style, and tries to have a playful attitude
1615 and makes gratuitous references to eating. But it is easier to follow
99 ### Relational Processing for Fun and Diversity - minikanren19-final6.pdf
1010
1111 * url: http://minikanren.org/workshop/2019/minikanren19-final6.pdf
12 * rating: TODO
1312
1413 .
1514
1615 ### Relational Interpreters for Search Problems - minikanren19-final3.pdf
1716
1817 * url: http://minikanren.org/workshop/2019/minikanren19-final3.pdf
19 * rating: TODO
2018
2119 .
2220
2321 ### An Empirical Study of Partial Deduction for miniKanren - minikanren-2020-paper2.pdf
2422
2523 * url: http://minikanren.org/workshop/2020/minikanren-2020-paper2.pdf
26 * rating: TODO
2724
2825 .
99 ### clojure - conda, condi, conde, condu - Stack Overflow
1010
1111 * url: https://stackoverflow.com/questions/10843563/conda-condi-conde-condu
12 * rating: 1
1312
1413 .
1514
1615 ### clojure - Understanding Mini-Kanren\'s Execution Model - Stack Overflow
1716
1817 * url: https://stackoverflow.com/questions/10118292/understanding-mini-kanrens-execution-model
19 * rating: 1
2018
2119 .
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 miniKanren
13 ---------------
14
15 ### The Reasoned Schemer
16
17 * rating: 1
18
19 .
20
21 ### Relational Processing for Fun and Diversity - minikanren19-final6.pdf
22
23 * rating: TODO
24
25 .
26
27 ### Relational Interpreters for Search Problems - minikanren19-final3.pdf
28
29 * rating: TODO
30
31 .
32
33 ### An Empirical Study of Partial Deduction for miniKanren - minikanren-2020-paper2.pdf
34
35 * rating: TODO
36
37 .
38
39 ### clojure - conda, condi, conde, condu - Stack Overflow
40
41 * rating: 1
42
43 .
44
45 ### clojure - Understanding Mini-Kanren\'s Execution Model - Stack Overflow
46
47 * rating: 1
48
49 .
50
99 ### Learn How to Develop and Publish an NPM Package
1010
1111 * url: https://auth0.com/blog/developing-npm-packages/
12 * rating: 1
1312
1413 .
1514
1615 ### node.js - "npm install" hangs on sill: idealTree build - Stack Overflow
1716
1817 * url: https://stackoverflow.com/questions/70865039/npm-install-hangs-on-sill-idealtree-build
19 * rating: 1
2018
2119 .
2220
2321 ### node.js - npm install hangs on loadIdealTree:loadAllDepsIntoIdealTree: sill install loadIdealTree - Stack Overflow
2422
2523 * url: https://stackoverflow.com/questions/50522376/npm-install-hangs-on-loadidealtreeloadalldepsintoidealtree-sill-install-loadid?rq=3
26 * rating: 1
2724
2825 .
2926
3027 ### node.js - Speeding up the npm install - Stack Overflow
3128
3229 * url: https://stackoverflow.com/questions/22077725/speeding-up-the-npm-install
33 * rating: 1
3430
3531 .
3632
3733 ### node.js - What\'s the difference between tilde(\~) and caret(\^) in package.json? - Stack Overflow
3834
3935 * url: https://stackoverflow.com/questions/22343224/whats-the-difference-between-tilde-and-caret-in-package-json
40 * rating: 1
4136
4237 .
4338
4439 ### How to install an npm package from GitHub directly? - Stack Overflow
4540
4641 * url: https://stackoverflow.com/questions/17509669/how-to-install-an-npm-package-from-github-directly
47 * rating: 1
4842
4943 .
5044
5145 ### How to view the dependency tree of a given npm module? - Stack Overflow
5246
5347 * url: https://stackoverflow.com/questions/25997519/how-to-view-the-dependency-tree-of-a-given-npm-module
54 * rating: 1
5548
5649 .
5750
5851 ### Getting Started \| Vite
5952
6053 * url: https://vitejs.dev/guide/
61 * rating: 1
6254
6355 .
0 Commentary by Chris Pressey
1 ===========================
2
3 <!--
4 Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
5
6 SPDX-License-Identifier: CC-BY-ND-4.0
7 -->
8
9 This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
10 exception: the ratings may be freely used for any purpose with no limitations.
11
12 npm
13 ---------------
14
15 ### Learn How to Develop and Publish an NPM Package
16
17 * rating: 1
18
19 .
20
21 ### node.js - "npm install" hangs on sill: idealTree build - Stack Overflow
22
23 * rating: 1
24
25 .
26
27 ### node.js - npm install hangs on loadIdealTree:loadAllDepsIntoIdealTree: sill install loadIdealTree - Stack Overflow
28
29 * rating: 1
30
31 .
32
33 ### node.js - Speeding up the npm install - Stack Overflow
34
35 * rating: 1
36
37 .
38
39 ### node.js - What\'s the difference between tilde(\~) and caret(\^) in package.json? - Stack Overflow
40
41 * rating: 1
42
43 .
44
45 ### How to install an npm package from GitHub directly? - Stack Overflow
46
47 * rating: 1
48
49 .
50
51 ### How to view the dependency tree of a given npm module? - Stack Overflow
52
53 * rating: 1
54
55 .
56
57 ### Getting Started \| Vite
58
59 * rating: 1
60
61 .
62
77 import json
88 import re
99 import os
10 import subprocess
1011
1112 from feedmark.loader import read_document_from
1213
2122
2223 def main(args):
2324 topic = args[0]
25 outdir = os.path.join(topic, "src", "commentary")
26 os.makedirs(outdir, exist_ok=True)
27 outfilename = os.path.join(outdir, "Chris Pressey.md")
28 if os.path.exists(outfilename):
29 raise OSError("{} already exists".format(outfilename))
2430
25 print("""\
31 sections = []
32 sections += load_feedmark_sections(topic, "Books.md")
33 sections += load_feedmark_sections(topic, "Papers.md")
34 sections += load_feedmark_sections(topic, "Webpages.md")
35 sections += load_feedmark_sections(topic, "Repositories.md")
36
37 with open(outfilename, 'w') as f:
38
39 f.write("""\
2640 Commentary by Chris Pressey
2741 ===========================
2842
3751
3852 {}
3953 ---------------
54
4055 """.format("SPDX-License-Identifier", topic))
41 sections = []
42 sections += load_feedmark_sections(topic, "Books.md")
43 sections += load_feedmark_sections(topic, "Papers.md")
44 sections += load_feedmark_sections(topic, "Webpages.md")
45 sections += load_feedmark_sections(topic, "Repositories.md")
56 for entry in sections:
57 f.write("### {}\n\n".format(entry["title"]))
58 f.write("* rating: {}\n\n".format(entry["properties"].get("rating", "TODO")))
59 f.write(".\n\n")
4660
47 for entry in sections:
48 print("### " + entry["title"])
49 print("")
50 print("* rating: " + entry["properties"].get("rating", "TODO"))
51 print("")
52 print(".")
53 print("")
61 subprocess.run("sed -i '/^\* rating/d' \"{}\"/src/*.md".format(topic), shell=True)
5462
63 # sed -i '/^\* rating/d' "$TOPIC"/src/*.md
64 # grep -r 'rating:' | grep -v commentary | sort
5565
5666 if __name__ == "__main__":
5767 import sys