Commit 86a226c9e45b7a5b790a870f8ac5335d1f88d833 - The-Glosscubator

Fix how online links are formatted. Chris Pressey 10 months ago

5 changed file(s) with 147 addition(s) and 143 deletion(s). Raw diff Collapse all Expand all

+17

-17

by-rating/Classics.md less more

18	18
19	19	### Algebraic Logic
20	20
21		* [A Formalization of Set Theory without Variables]([archive.org](https://archive.org/details/formalizationofs0000tars_d3r8))
	21	* A Formalization of Set Theory without Variables ([archive.org](https://archive.org/details/formalizationofs0000tars_d3r8))
22	22
23	23	### Compiler Construction
24	24
25		* [Compilers: Principles, Techniques, and Tools (1st Ed.)]([archive.org](https://archive.org/details/addison-wesley-aho-sethi-ullman-compilers-principles-techniques-and-tools))
	25	* Compilers: Principles, Techniques, and Tools (1st Ed.) ([archive.org](https://archive.org/details/addison-wesley-aho-sethi-ullman-compilers-principles-techniques-and-tools))
26	26
27	27	### Lambda Calculus
28	28
29		* [The Calculi of Lambda-Conversion]([archive.org](https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941))
	29	* The Calculi of Lambda-Conversion ([archive.org](https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941))
30	30
31	31	### Lisp
32	32
33		* [Lisp 1.5 Programmer's Manual]([archive.org](https://archive.org/details/DTIC_AD0406138))
34		* [The Little Lisper]([archive.org](https://archive.org/details/tlLISP))
	33	* Lisp 1.5 Programmer's Manual ([archive.org](https://archive.org/details/DTIC_AD0406138))
	34	* The Little Lisper ([archive.org](https://archive.org/details/tlLISP))
35	35
36	36	### Logic
37	37
38		* [Mathematical Logic]([archive.org](https://archive.org/details/mathematicallogi0000klee))
39		* [Mathematical Logic]([archive.org](https://archive.org/details/QUINEMathematicalLogic))
	38	* Mathematical Logic ([archive.org](https://archive.org/details/mathematicallogi0000klee))
	39	* Mathematical Logic ([archive.org](https://archive.org/details/QUINEMathematicalLogic))
40	40
41	41	### Numerical Analysis
42	42
43		* [Numerical Recipes]([archive.org](https://archive.org/details/NumericalRecipes))
	43	* Numerical Recipes ([archive.org](https://archive.org/details/NumericalRecipes))
44	44
45	45	### Prolog
46	46
47		* [Programming in PROLOG]([archive.org](https://archive.org/details/programminginpro00cloc))
	47	* Programming in PROLOG ([archive.org](https://archive.org/details/programminginpro00cloc))
48	48
49	49	### Software Engineering
50	50
51		* [Advanced Programming in the Unix Environment]([archive.org](https://archive.org/details/isbn_9789812358813))
	51	* Advanced Programming in the Unix Environment ([archive.org](https://archive.org/details/isbn_9789812358813))
52	52
53	53	Classics Papers
54	54	--------------

59	59
60	60	### Attribute Grammars
61	61
62		* [Semantics of Context-Free Languages]([www.khoury.northeastern.edu](https://www.khoury.northeastern.edu/home/chadwick/files/knuth.pdf))
	62	* Semantics of Context-Free Languages ([www.khoury.northeastern.edu](https://www.khoury.northeastern.edu/home/chadwick/files/knuth.pdf))
63	63
64	64	### Formal Language
65	65

71	71
72	72	### Logic Programming
73	73
74		* [The Semantics of Predicate Logic as a Programming Language]([doc.ic.ac.uk](https://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf))
	74	* The Semantics of Predicate Logic as a Programming Language ([doc.ic.ac.uk](https://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf))
75	75
76	76	### PLDI
77	77
78		* [Fundamental Concepts in Programming Languages]([ics.uci.edu](https://ics.uci.edu/~jajones/INF102-S18/readings/05_stratchey_1967.pdf))
79		* [Definitional interpreters for higher-order programming languages]([homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-1998.pdf) (PDF))
	78	* Fundamental Concepts in Programming Languages ([ics.uci.edu](https://ics.uci.edu/~jajones/INF102-S18/readings/05_stratchey_1967.pdf))
	79	* Definitional interpreters for higher-order programming languages ([homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/wadler/papers/papers-we-love/reynolds-definitional-interpreters-1998.pdf) (PDF))
80	80
81	81	### Partial Evaluation
82	82

85	85
86	86	### Refinement Calculus
87	87
88		* [Can Programming Be Liberated from the von Neumann Style?]([dl.acm.org](https://dl.acm.org/doi/10.1145/359576.359579))
	88	* Can Programming Be Liberated from the von Neumann Style? ([dl.acm.org](https://dl.acm.org/doi/10.1145/359576.359579))
89	89
90	90	### Software Engineering
91	91
92		* [Programming as Theory Building]([pages.cs.wisc.edu](https://pages.cs.wisc.edu/~remzi/Naur.pdf) (PDF))
	92	* Programming as Theory Building ([pages.cs.wisc.edu](https://pages.cs.wisc.edu/~remzi/Naur.pdf) (PDF))
93	93
94	94	### Topology
95	95
96		* [The Lattice of Topologies: Structure and Complementation]([www.ams.org](https://www.ams.org/journals/tran/1966-122-02/S0002-9947-1966-0190893-2/S0002-9947-1966-0190893-2.pdf) (PDF))
	96	* The Lattice of Topologies: Structure and Complementation ([www.ams.org](https://www.ams.org/journals/tran/1966-122-02/S0002-9947-1966-0190893-2/S0002-9947-1966-0190893-2.pdf) (PDF))
97	97
98	98	Classics Repos
99	99	--------------

+47

-47

by-rating/Top-rated.md less more

141	141
142	142	### Algebraic Logic
143	143
144		* [Logic as Algebra]([archive.org](https://archive.org/details/logicasalgebra0000halm))
	144	* Logic as Algebra ([archive.org](https://archive.org/details/logicasalgebra0000halm))
145	145
146	146	### BASIC
147	147
148		* [Write your own Adventure Programs for your Microcomputer]([usborne.com](https://usborne.com/gb/books/computer-and-coding-books))
	148	* Write your own Adventure Programs for your Microcomputer ([usborne.com](https://usborne.com/gb/books/computer-and-coding-books))
149	149
150	150	### Commodore 64
151	151
152		* [Commodore 64 Programmer's Reference Guide]([www.commodore.ca](https://www.commodore.ca/manuals/c64_programmers_reference/c64-programmers_reference.htm))
153		* [1001 Things to Do With your Commodore 64]([archive.org](https://archive.org/details/1001_Things_to_do_with_your_Commodore_64_1984_TAB_Books))
	152	* Commodore 64 Programmer's Reference Guide ([www.commodore.ca](https://www.commodore.ca/manuals/c64_programmers_reference/c64-programmers_reference.htm))
	153	* 1001 Things to Do With your Commodore 64 ([archive.org](https://archive.org/details/1001_Things_to_do_with_your_Commodore_64_1984_TAB_Books))
154	154
155	155	### Constraint Programming
156	156
157		* [Constraint Programming Languages: Their Specification and Generation]([archive.org](https://archive.org/details/constraintprogra0000lele))
	157	* Constraint Programming Languages: Their Specification and Generation ([archive.org](https://archive.org/details/constraintprogra0000lele))
158	158
159	159	### Coq
160	160
161		* [Software Foundations]([softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/))
	161	* Software Foundations ([softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/))
162	162
163	163	### Electronics
164	164
165		* [Getting Started in Electronics]([archive.org](https://archive.org/details/gettingstartedin00mims))
	165	* Getting Started in Electronics ([archive.org](https://archive.org/details/gettingstartedin00mims))
166	166
167	167	### Game Design
168	168
169		* [The Art of Computer Game Design]([archive.org](https://archive.org/details/artofcomputergam00chri))
	169	* The Art of Computer Game Design ([archive.org](https://archive.org/details/artofcomputergam00chri))
170	170
171	171	### Literature
172	172
173		* [I am a Cat]([archive.org](https://archive.org/details/iamcat0000nats) (2002 edition))
	173	* I am a Cat ([archive.org](https://archive.org/details/iamcat0000nats) (2002 edition))
174	174
175	175	### Lua
176	176
177		* [Programming in Lua (first edition)]([www.lua.org](https://www.lua.org/pil/contents.html))
	177	* Programming in Lua (first edition) ([www.lua.org](https://www.lua.org/pil/contents.html))
178	178
179	179	### Mathematics
180	180
181		* [The Magical Maze]([archive.org](https://archive.org/details/magicalmazeseein0000stew))
	181	* The Magical Maze ([archive.org](https://archive.org/details/magicalmazeseein0000stew))
182	182
183	183	### Modal Logic
184	184
185		* [Introductory Modal Logic]([archive.org](https://archive.org/details/introductorymoda00kony))
186		* [First Steps in Modal Logic]([archive.org](https://archive.org/details/firststepsinmoda0000popk))
	185	* Introductory Modal Logic ([archive.org](https://archive.org/details/introductorymoda00kony))
	186	* First Steps in Modal Logic ([archive.org](https://archive.org/details/firststepsinmoda0000popk))
187	187
188	188	### PLDI
189	189
190		* [A Practical Introduction to Denotational Semantics]([archive.org](https://archive.org/details/practicalintrodu0000alli))
191		* [Formal Syntax and Semantics of Programming Languages]([archive.org](https://archive.org/details/formalsyntaxsema0000slon))
	190	* A Practical Introduction to Denotational Semantics ([archive.org](https://archive.org/details/practicalintrodu0000alli))
	191	* Formal Syntax and Semantics of Programming Languages ([archive.org](https://archive.org/details/formalsyntaxsema0000slon))
192	192
193	193	### Pascal
194	194
195		* [Programming Your Own Adventure Games in Pascal]([archive.org](https://archive.org/details/programming-your-own-adventure-games-in-pascal))
	195	* Programming Your Own Adventure Games in Pascal ([archive.org](https://archive.org/details/programming-your-own-adventure-games-in-pascal))
196	196
197	197	### Philosophy
198	198
199		* [The Cognitive Connection: Thought and Language in Man and Machine]([archive.org](https://archive.org/details/cognitiveconnect0000levi))
	199	* The Cognitive Connection: Thought and Language in Man and Machine ([archive.org](https://archive.org/details/cognitiveconnect0000levi))
200	200
201	201	### Probability Theory
202	202
203		* [Probability Theory]([www.med.mcgill.ca](http://www.med.mcgill.ca/epidemiology/hanley/bios601/GaussianModel/JaynesProbabilityTheory.pdf))
	203	* Probability Theory ([www.med.mcgill.ca](http://www.med.mcgill.ca/epidemiology/hanley/bios601/GaussianModel/JaynesProbabilityTheory.pdf))
204	204
205	205	### Prolog
206	206
207		* [The Art of Prolog]([archive.org](https://archive.org/details/artofprologadvan0000ster))
	207	* The Art of Prolog ([archive.org](https://archive.org/details/artofprologadvan0000ster))
208	208
209	209	### Relational Programming
210	210
211		* [Relational Methods in Computer Science]([archive.org](https://archive.org/details/relationalmethod0000unse))
	211	* Relational Methods in Computer Science ([archive.org](https://archive.org/details/relationalmethod0000unse))
212	212
213	213	### Retrocomputing
214	214
215		* [Microprocessor Programming for Computer Hobbyists]([archive.org](https://archive.org/details/microprocessorpr0000grah))
	215	* Microprocessor Programming for Computer Hobbyists ([archive.org](https://archive.org/details/microprocessorpr0000grah))
216	216
217	217	### Software Engineering
218	218
219		* [The Mythical Man-Month]([archive.org](https://archive.org/details/MythicalManMonth))
220		* [Object-Oriented Modelling and Design]([archive.org](https://archive.org/details/objectorientedmo00rumb))
	219	* The Mythical Man-Month ([archive.org](https://archive.org/details/MythicalManMonth))
	220	* Object-Oriented Modelling and Design ([archive.org](https://archive.org/details/objectorientedmo00rumb))
221	221
222	222	### Theory of Computation
223	223
224		* [Computation: Finite and Infinite Machines]([archive.org](https://archive.org/details/computationfinit0000mins))
225		* [The Universal Turing Machine]([archive.org](https://archive.org/details/universalturingm0000unse))
226		* [Theory of Deductive Systems and its Applications]([archive.org](https://archive.org/details/TheoryofDe_00_Masl))
	224	* Computation: Finite and Infinite Machines ([archive.org](https://archive.org/details/computationfinit0000mins))
	225	* The Universal Turing Machine ([archive.org](https://archive.org/details/universalturingm0000unse))
	226	* Theory of Deductive Systems and its Applications ([archive.org](https://archive.org/details/TheoryofDe_00_Masl))
227	227
228	228	### Topology
229	229
230		* [Counterexamples in Topology]([archive.org](https://archive.org/details/counterexamplesi0000stee))
	230	* Counterexamples in Topology ([archive.org](https://archive.org/details/counterexamplesi0000stee))
231	231
232	232	Top-rated Papers
233	233	--------------
234	234
235	235	### Combinatorics
236	236
237		* [Boltzmann Samplers for the Random Generation of Combinatorial Structures]([algo.inria.fr](https://algo.inria.fr/flajolet/Publications/DuFlLoSc04.pdf) (PDF))
238		* [What Lies Between Order and Chaos?]([csc.ucdavis.edu](https://csc.ucdavis.edu/~cmg/compmech/tutorials/wlboac.pdf) (PDF))
	237	* Boltzmann Samplers for the Random Generation of Combinatorial Structures ([algo.inria.fr](https://algo.inria.fr/flajolet/Publications/DuFlLoSc04.pdf) (PDF))
	238	* What Lies Between Order and Chaos? ([csc.ucdavis.edu](https://csc.ucdavis.edu/~cmg/compmech/tutorials/wlboac.pdf) (PDF))
239	239
240	240	### Compiler Construction
241	241
242		* [The essence of compiling with continuations]([web.archive.org](https://web.archive.org/web/20210423174105/http://www.cs.rice.edu/~javaplt/311/Readings/essence-retro.pdf) (PDF))
	242	* The essence of compiling with continuations ([web.archive.org](https://web.archive.org/web/20210423174105/http://www.cs.rice.edu/~javaplt/311/Readings/essence-retro.pdf) (PDF))
243	243
244	244	### Computational Complexity
245	245
246		* [Why Philosophers Should Care About Computational Complexity]([www.scottaaronson.com](https://www.scottaaronson.com/papers/philos.pdf) (PDF))
	246	* Why Philosophers Should Care About Computational Complexity ([www.scottaaronson.com](https://www.scottaaronson.com/papers/philos.pdf) (PDF))
247	247
248	248	### Equational Logic
249	249

251	251
252	252	### Functional Programming
253	253
254		* [A tutorial on the universality and expressiveness of fold]([www.cs.nott.ac.uk](https://www.cs.nott.ac.uk/~pszgmh/fold.pdf) (PDF))
	254	* A tutorial on the universality and expressiveness of fold ([www.cs.nott.ac.uk](https://www.cs.nott.ac.uk/~pszgmh/fold.pdf) (PDF))
255	255
256	256	### Lambda Calculus
257	257
258		* [The Lambda Calculus is Algebraic]([www.mscs.dal.ca](https://www.mscs.dal.ca/~selinger/papers/combinatory.pdf))
	258	* The Lambda Calculus is Algebraic ([www.mscs.dal.ca](https://www.mscs.dal.ca/~selinger/papers/combinatory.pdf))
259	259
260	260	### Mathematics
261	261
262		* [Infinity - A simple, but not too simple introduction]([arxiv.org](https://arxiv.org/abs/1506.06319))
	262	* Infinity - A simple, but not too simple introduction ([arxiv.org](https://arxiv.org/abs/1506.06319))
263	263
264	264	### PLDI
265	265
266		* [Trampolined style]([dl.acm.org](https://dl.acm.org/doi/abs/10.1145/317636.317779))
	266	* Trampolined style ([dl.acm.org](https://dl.acm.org/doi/abs/10.1145/317636.317779))
267	267
268	268	### Reactive Systems
269	269
270		* [Statecharts]([www.inf.ed.ac.uk](https://www.inf.ed.ac.uk/teaching/courses/seoc/2005_2006/resources/statecharts.pdf) (PDF))
271		* [State Machines for Event-Driven Systems]([barrgroup.com](https://barrgroup.com/embedded-systems/how-to/state-machines-event-driven-systems))
272		* [Misunderstandings about state machines]([www.stateworks.com](https://www.stateworks.com/active/download/wagf04-2-state-machine-misunderstandings.pdf))
	270	* Statecharts ([www.inf.ed.ac.uk](https://www.inf.ed.ac.uk/teaching/courses/seoc/2005_2006/resources/statecharts.pdf) (PDF))
	271	* State Machines for Event-Driven Systems ([barrgroup.com](https://barrgroup.com/embedded-systems/how-to/state-machines-event-driven-systems))
	272	* Misunderstandings about state machines ([www.stateworks.com](https://www.stateworks.com/active/download/wagf04-2-state-machine-misunderstandings.pdf))
273	273
274	274	### Refinement Calculus
275	275
276		* [Algorithmics]([ir.cwi.nl](https://ir.cwi.nl/pub/2686/2686D.pdf) (PDF))
277		* [Laws of Programming]([ox.ac.uk](https://www.cs.ox.ac.uk/bill.roscoe/publications/20.pdf) (PDF))
278		* [Algebraic Identities for Program Calculation]([academic.oup.com](https://academic.oup.com/comjnl/article-pdf/32/2/122/1445670/320122.pdf) (PDF))
	276	* Algorithmics ([ir.cwi.nl](https://ir.cwi.nl/pub/2686/2686D.pdf) (PDF))
	277	* Laws of Programming ([ox.ac.uk](https://www.cs.ox.ac.uk/bill.roscoe/publications/20.pdf) (PDF))
	278	* Algebraic Identities for Program Calculation ([academic.oup.com](https://academic.oup.com/comjnl/article-pdf/32/2/122/1445670/320122.pdf) (PDF))
279	279
280	280	### Software Engineering
281	281
282		* [Why software jewels are rare]([www.yodaiken.com](https://www.yodaiken.com/papers/Why_software_jewels_are_rare.pdf) (PDF))
	282	* Why software jewels are rare ([www.yodaiken.com](https://www.yodaiken.com/papers/Why_software_jewels_are_rare.pdf) (PDF))
283	283
284	284	### Specification
285	285

287	287
288	288	### Theorem Proving
289	289
290		* [The Future of Mathematics?]([www.andrew.cmu.edu](https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf) (PDF))
	290	* The Future of Mathematics? ([www.andrew.cmu.edu](https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf) (PDF))
291	291
292	292	### Type Systems
293	293
294		* [Should Your Specification Language Be Typed?]([lamport.azurewebsites.net](http://lamport.azurewebsites.net/pubs/lamport-types.pdf) (PDF))
295		* [On Understanding Data Abstraction, Revisited]([cs.utexas.edu](https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf) (PDF))
296		* [In Search of Types]([kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/srk21/papers/kell14in-author-version.pdf) (PDF))
297		* [Unfolding Abstract Datatypes]([www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf))
	294	* Should Your Specification Language Be Typed? ([lamport.azurewebsites.net](http://lamport.azurewebsites.net/pubs/lamport-types.pdf) (PDF))
	295	* On Understanding Data Abstraction, Revisited ([cs.utexas.edu](https://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf) (PDF))
	296	* In Search of Types ([kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/srk21/papers/kell14in-author-version.pdf) (PDF))
	297	* Unfolding Abstract Datatypes ([www.cs.ox.ac.uk](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf))
298	298
299	299	Top-rated Repos
300	300	--------------

+71

-71

by-rating/Unrated.md less more

40	40
41	41	### Agile Development
42	42
43		* [Agile Systems Engineering]([archive.org](https://archive.org/details/agilesystemsengi0000doug))
	43	* Agile Systems Engineering ([archive.org](https://archive.org/details/agilesystemsengi0000doug))
44	44
45	45	### Artificial Intelligence
46	46
47		* [Building Problem Solvers]([archive.org](https://archive.org/details/buildingproblems0000forb))
	47	* Building Problem Solvers ([archive.org](https://archive.org/details/buildingproblems0000forb))
48	48
49	49	### Attribute Grammars
50	50
51		* [A Compiler Generator for Microcomputers]([archive.org](https://archive.org/details/compilergenerato0000rech))
	51	* A Compiler Generator for Microcomputers ([archive.org](https://archive.org/details/compilergenerato0000rech))
52	52
53	53	### Category Theory
54	54
55		* [Categories, types, and structures]([www.di.ens.fr](https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf))
	55	* Categories, types, and structures ([www.di.ens.fr](https://www.di.ens.fr/users/longo/files/CategTypesStructures/book.pdf))
56	56
57	57	### Computational Complexity
58	58
59		* [Computational Complexity]([archive.org](https://archive.org/details/computationalcom0000wagn))
	59	* Computational Complexity ([archive.org](https://archive.org/details/computationalcom0000wagn))
60	60
61	61	### Coq
62	62
63		* [Certified Programming with Dependent Types]([archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes))
64		* [Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft)]([www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf))
	63	* Certified Programming with Dependent Types ([archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes))
	64	* Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft) ([www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf))
65	65
66	66	### Equational Logic
67	67
68		* [Canonical Equational Proofs]([archive.org](https://archive.org/details/canonicalequatio0000bach))
	68	* Canonical Equational Proofs ([archive.org](https://archive.org/details/canonicalequatio0000bach))
69	69
70	70	### Formal Language
71	71
72		* [Introduction to Formal Languages]([archive.org](https://archive.org/details/introductiontofo0000reve))
73		* [Natural Language Processing Techniques in Prolog]([cs.union.edu](https://cs.union.edu/~striegnk/courses/nlp-with-prolog/html/index.html))
74		* [Programs, Grammars, Arguments]([archive.org](https://archive.org/details/flooved3381))
	72	* Introduction to Formal Languages ([archive.org](https://archive.org/details/introductiontofo0000reve))
	73	* Natural Language Processing Techniques in Prolog ([cs.union.edu](https://cs.union.edu/~striegnk/courses/nlp-with-prolog/html/index.html))
	74	* Programs, Grammars, Arguments ([archive.org](https://archive.org/details/flooved3381))
75	75
76	76	### Functional Programming
77	77
78		* [Purely Functional Data Structures]([archive.org](https://archive.org/details/okasaki-purely-functional-data-structures))
	78	* Purely Functional Data Structures ([archive.org](https://archive.org/details/okasaki-purely-functional-data-structures))
79	79
80	80	### Lambda Calculus
81	81
82		* [Introduction to Combinators and the Lambda Calculus]([archive.org](https://archive.org/details/introductiontoco0000hind))
	82	* Introduction to Combinators and the Lambda Calculus ([archive.org](https://archive.org/details/introductiontoco0000hind))
83	83
84	84	### Linguistics
85	85
86		* [Essentials of English Grammar]([archive.org](https://archive.org/details/essentialsofengl0000lang))
87		* [English Transformational Grammar]([archive.org](https://archive.org/details/englishtransform0000jaco_p1k5))
88		* [Modern English Linguistics]([archive.org](https://archive.org/details/modernenglishlin0000brod))
89		* [Towards a Semantic Description of English]([archive.org](https://archive.org/details/towardssemanticd0000leec))
90		* [An Introduction to Unification-based Approaches to Grammar]([dash.harvard.edu](https://dash.harvard.edu/bitstream/handle/1/11576719/shieber-uagf-distrib-130816_0.pdf))
91		* [The Language Complexity Game]([archive.org](https://archive.org/details/languagecomplexi00rist))
	86	* Essentials of English Grammar ([archive.org](https://archive.org/details/essentialsofengl0000lang))
	87	* English Transformational Grammar ([archive.org](https://archive.org/details/englishtransform0000jaco_p1k5))
	88	* Modern English Linguistics ([archive.org](https://archive.org/details/modernenglishlin0000brod))
	89	* Towards a Semantic Description of English ([archive.org](https://archive.org/details/towardssemanticd0000leec))
	90	* An Introduction to Unification-based Approaches to Grammar ([dash.harvard.edu](https://dash.harvard.edu/bitstream/handle/1/11576719/shieber-uagf-distrib-130816_0.pdf))
	91	* The Language Complexity Game ([archive.org](https://archive.org/details/languagecomplexi00rist))
92	92
93	93	### Literature
94	94
95		* [The Secret Agent]([gutenberg.org](https://www.gutenberg.org/ebooks/974))
96		* [The Good Soldier]([gutenberg.org](https://www.gutenberg.org/ebooks/2775))
97		* [The Counterfeiters]([archive.org](https://archive.org/details/counterfeiters00gide))
98		* [Mr Pye]([archive.org](https://archive.org/details/mrpye0000peak_a2p9))
99		* [The Great Gatsby by F. Scott Fitzgerald \\| Project Gutenberg]([gutenberg.org](https://gutenberg.org/ebooks/64317))
	95	* The Secret Agent ([gutenberg.org](https://www.gutenberg.org/ebooks/974))
	96	* The Good Soldier ([gutenberg.org](https://www.gutenberg.org/ebooks/2775))
	97	* The Counterfeiters ([archive.org](https://archive.org/details/counterfeiters00gide))
	98	* Mr Pye ([archive.org](https://archive.org/details/mrpye0000peak_a2p9))
	99	* The Great Gatsby by F. Scott Fitzgerald \\| Project Gutenberg ([gutenberg.org](https://gutenberg.org/ebooks/64317))
100	100
101	101	### Logic
102	102
103		* [Logic]([archive.org](https://archive.org/details/logic00hodg))
104		* [Mathematical logic and formalized theories]([archive.org](https://archive.org/details/mathematicallogi0000roge))
105		* [The Blackwell Guide To Philosophical Logic]([archive.org](https://archive.org/details/lou-goble-the-blackwell-guide-to-philosophical-logic))
106		* [Handbook of Logic in Computer Science, Volume 1]([archive.org](https://archive.org/details/handbookoflogici0001unse_z8j4))
107		* [Handbook of Logic and Proof Techniques for Computer Science]([archive.org](https://archive.org/details/handbookoflogicp0000kran))
108		* [Simply Logical]([book.simply-logical.space](https://book.simply-logical.space/src/simply-logical.html))
	103	* Logic ([archive.org](https://archive.org/details/logic00hodg))
	104	* Mathematical logic and formalized theories ([archive.org](https://archive.org/details/mathematicallogi0000roge))
	105	* The Blackwell Guide To Philosophical Logic ([archive.org](https://archive.org/details/lou-goble-the-blackwell-guide-to-philosophical-logic))
	106	* Handbook of Logic in Computer Science, Volume 1 ([archive.org](https://archive.org/details/handbookoflogici0001unse_z8j4))
	107	* Handbook of Logic and Proof Techniques for Computer Science ([archive.org](https://archive.org/details/handbookoflogicp0000kran))
	108	* Simply Logical ([book.simply-logical.space](https://book.simply-logical.space/src/simply-logical.html))
109	109
110	110	### Logic Programming
111	111
112		* [Programming with Higher-Order Logic]([archive.org](https://archive.org/details/programmingwithh0000mill))
	112	* Programming with Higher-Order Logic ([archive.org](https://archive.org/details/programmingwithh0000mill))
113	113
114	114	### Numerical Analysis
115	115
116		* [An Introduction to Computer Simulation Methods: Applications to Physical Systems]([archive.org](https://archive.org/details/introductiontoco0000goul))
117		* [Inside SPICE]([archive.org](https://archive.org/details/kielkowski-inside-spice-1994))
	116	* An Introduction to Computer Simulation Methods: Applications to Physical Systems ([archive.org](https://archive.org/details/introductiontoco0000goul))
	117	* Inside SPICE ([archive.org](https://archive.org/details/kielkowski-inside-spice-1994))
118	118
119	119	### Partial Evaluation
120	120
121		* [Partial Evaluation and Automatic Program Generation]([www.itu.dk](http://www.itu.dk/people/sestoft/pebook/))
122		* [Partial evaluation : practice and theory]([archive.org](https://archive.org/details/springer_10.1007-3-540-47018-2))
	121	* Partial Evaluation and Automatic Program Generation ([www.itu.dk](http://www.itu.dk/people/sestoft/pebook/))
	122	* Partial evaluation : practice and theory ([archive.org](https://archive.org/details/springer_10.1007-3-540-47018-2))
123	123
124	124	### Philosophy
125	125
126		* [Patterns of Software: Tales from the Software Community]([archive.org](https://archive.org/details/PatternsOfSoftware))
	126	* Patterns of Software: Tales from the Software Community ([archive.org](https://archive.org/details/PatternsOfSoftware))
127	127
128	128	### Proof Theory
129	129
130		* [Basic Proof Theory]([archive.org](https://archive.org/details/basicprooftheory0000troe))
	130	* Basic Proof Theory ([archive.org](https://archive.org/details/basicprooftheory0000troe))
131	131
132	132	### Reactive Systems
133	133
134		* [Synchronous Programming of Reactive Systems]([web.archive.org](https://web.archive.org/web/20240413191204/http://www-verimag.imag.fr/~halbwach/newbook.pdf))
	134	* Synchronous Programming of Reactive Systems ([web.archive.org](https://web.archive.org/web/20240413191204/http://www-verimag.imag.fr/~halbwach/newbook.pdf))
135	135
136	136	### Refinement Calculus
137	137
138		* [a Practical Theory of Programming]([www.cs.toronto.edu](https://www.cs.toronto.edu/~hehner/aPToP/))
139		* [Refinement Calculus: A Systematic Introduction]([lara.epfl.ch](https://lara.epfl.ch/w/_media/sav08:backwright98refinementcalculus.pdf))
	138	* a Practical Theory of Programming ([www.cs.toronto.edu](https://www.cs.toronto.edu/~hehner/aPToP/))
	139	* Refinement Calculus: A Systematic Introduction ([lara.epfl.ch](https://lara.epfl.ch/w/_media/sav08:backwright98refinementcalculus.pdf))
140	140
141	141	### Retrocomputing
142	142
143		* [How to Build a Working Digital Computer]([archive.org](https://archive.org/details/howtobuildaworkingdigitalcomputer_jun67))
	143	* How to Build a Working Digital Computer ([archive.org](https://archive.org/details/howtobuildaworkingdigitalcomputer_jun67))
144	144
145	145	### Specification
146	146
147		* [Program specification and transformation]([archive.org](https://archive.org/details/programspecifica0000ifip))
148		* [Semantics, applications, and implementation of program generation]([archive.org](https://archive.org/details/springer_10.1007-3-540-44806-3))
	147	* Program specification and transformation ([archive.org](https://archive.org/details/programspecifica0000ifip))
	148	* Semantics, applications, and implementation of program generation ([archive.org](https://archive.org/details/springer_10.1007-3-540-44806-3))
149	149
150	150	### Theorem Proving
151	151
152		* [The Seventeen Provers of the World]([archive.org](https://archive.org/details/seventeenprovers00free))
153		* [Theorem Proving in Lean 4]([archive.org](https://leanprover.github.io/theorem_proving_in_lean4/))
	152	* The Seventeen Provers of the World ([archive.org](https://archive.org/details/seventeenprovers00free))
	153	* Theorem Proving in Lean 4 ([archive.org](https://leanprover.github.io/theorem_proving_in_lean4/))
154	154
155	155	### Theory of Computation
156	156
157		* [Theory of Recursive Functions and Effective Computability]([archive.org](https://archive.org/details/theoryofrecursiv00roge))
158		* [Computability Theory, Semantics, and Logic Programming]([archive.org](https://archive.org/details/computabilitythe0000fitt))
	157	* Theory of Recursive Functions and Effective Computability ([archive.org](https://archive.org/details/theoryofrecursiv00roge))
	158	* Computability Theory, Semantics, and Logic Programming ([archive.org](https://archive.org/details/computabilitythe0000fitt))
159	159
160	160	### Type Theory
161	161
162		* [Basic Simple Type Theory]([archive.org](https://archive.org/details/basicsimpletypet0000hind))
163		* [Type Theory and Functional Programming]([www.cs.kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf))
164		* [Programming in Martin-Löf’s Type Theory]([www.cse.chalmers.se](http://www.cse.chalmers.se/research/group/logic/book/))
	162	* Basic Simple Type Theory ([archive.org](https://archive.org/details/basicsimpletypet0000hind))
	163	* Type Theory and Functional Programming ([www.cs.kent.ac.uk](https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf))
	164	* Programming in Martin-Löf’s Type Theory ([www.cse.chalmers.se](http://www.cse.chalmers.se/research/group/logic/book/))
165	165
166	166	Unrated Papers
167	167	--------------

179	179
180	180	### Haskell
181	181
182		* [Faking it]([www.cambridge.org](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/faking-it-simulating-dependent-types-in-haskell/A904B84CA962F2D75578445B703F199A))
	182	* Faking it ([www.cambridge.org](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/faking-it-simulating-dependent-types-in-haskell/A904B84CA962F2D75578445B703F199A))
183	183
184	184	### Incompleteness
185	185
186		* [A Simple Character String Proof of the \"True but Unprovable\" Version of Goedel\'s First Incompleteness Theorem]([arxiv.org](https://arxiv.org/abs/1402.7253))
187		* [A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points]([arxiv.org](https://arxiv.org/abs/math/0305282))
188		* [Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles]([jstor](https://www.jstor.org/stable/2695030))
	186	* A Simple Character String Proof of the \"True but Unprovable\" Version of Goedel\'s First Incompleteness Theorem ([arxiv.org](https://arxiv.org/abs/1402.7253))
	187	* A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points ([arxiv.org](https://arxiv.org/abs/math/0305282))
	188	* Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles ([jstor](https://www.jstor.org/stable/2695030))
189	189
190	190	### Macros
191	191

194	194
195	195	### Modal Logic
196	196
197		* [The Relationship between the Topological Properties and Common Modal Logics]([pubs.sciepub.com](https://pubs.sciepub.com/jmsa/4/1/5/index.html))
198		* [Topological semantics of modal logic]([tsinghualogic.net](https://tsinghualogic.net/JRC/wp-content/uploads/2021/07/5thLecturewithReference.pdf))
199		* [Topology, Connectedness, and Modal Logic]([www.dcs.bbk.ac.uk](https://www.dcs.bbk.ac.uk/~roman/papers/aiml-08-55.pdf))
200		* [A Modal Walk Through Space]([web.archive.org](https://web.archive.org/web/20221001044857/https://www.cs.rug.nl/~aiellom/publications/lops2.pdf))
	197	* The Relationship between the Topological Properties and Common Modal Logics ([pubs.sciepub.com](https://pubs.sciepub.com/jmsa/4/1/5/index.html))
	198	* Topological semantics of modal logic ([tsinghualogic.net](https://tsinghualogic.net/JRC/wp-content/uploads/2021/07/5thLecturewithReference.pdf))
	199	* Topology, Connectedness, and Modal Logic ([www.dcs.bbk.ac.uk](https://www.dcs.bbk.ac.uk/~roman/papers/aiml-08-55.pdf))
	200	* A Modal Walk Through Space ([web.archive.org](https://web.archive.org/web/20221001044857/https://www.cs.rug.nl/~aiellom/publications/lops2.pdf))
201	201
202	202	### Model Checking
203	203

206	206
207	207	### Name Binding
208	208
209		* [Foundational Aspects of Syntax]([web.archive.org](https://web.archive.org/web/20240304215325/https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lambda-trees.pdf))
210		* [Abstract Syntax for Variable Binders]([web.archive.org](https://web.archive.org/web/20240415115853/http://www.lix.polytechnique.fr/~dale/papers/cl2000.pdf))
	209	* Foundational Aspects of Syntax ([web.archive.org](https://web.archive.org/web/20240304215325/https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lambda-trees.pdf))
	210	* Abstract Syntax for Variable Binders ([web.archive.org](https://web.archive.org/web/20240415115853/http://www.lix.polytechnique.fr/~dale/papers/cl2000.pdf))
211	211	* [A Metalanguage for Programming with Bound Names Modulo Renaming](https://www.cl.cam.ac.uk/~amp12/papers/metpbn/metpbn.pdf)
212	212	* [I am not a Number, I am a Free Variable](http://www.e-pig.org/downloads/notanum.pdf)
213	213	* [A Type and Scope Safe Universe of Syntaxes with Binding](https://pure.strath.ac.uk/ws/portalfiles/portal/114903157/Allais_etal_ICFP2018_A_type_and_scope_safe_universe_of_syntaxes_with_binding.pdf)

218	218
219	219	### Programming Languages
220	220
221		* [Synchronous Functional Programming: The Lucid Synchrone Experiment]([www.di.ens.fr](https://www.di.ens.fr/~pouzet/bib/chap_lucid_synchrone_english_iste08.pdf) (PDF))
	221	* Synchronous Functional Programming: The Lucid Synchrone Experiment ([www.di.ens.fr](https://www.di.ens.fr/~pouzet/bib/chap_lucid_synchrone_english_iste08.pdf) (PDF))
222	222
223	223	### Refinement Calculus
224	224
225		* [Correctness Preserving Program Refinements]([ir.cwl.nl](https://ir.cwi.nl/pub/12990))
	225	* Correctness Preserving Program Refinements ([ir.cwl.nl](https://ir.cwi.nl/pub/12990))
226	226
227	227	### Relational Programming
228	228

232	232
233	233	### Theorem Proving
234	234
235		* [[0707.0926] Theorem proving support in programming language semantics]([arxiv.org](https://arxiv.org/abs/0707.0926))
236		* [Towards self-verification of HOL Light]([www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf))
237		* [A Self-Verifying Theorem Prover]([www.kookamara.com](https://www.kookamara.com/jared/dissertation.pdf))
	235	* [0707.0926] Theorem proving support in programming language semantics ([arxiv.org](https://arxiv.org/abs/0707.0926))
	236	* Towards self-verification of HOL Light ([www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf))
	237	* A Self-Verifying Theorem Prover ([www.kookamara.com](https://www.kookamara.com/jared/dissertation.pdf))
238	238
239	239	### Topology
240	240
241		* [Finite Topological Spaces]([www.math.uchicago.edu](https://www.math.uchicago.edu/~may/MISC/FiniteSpaces.pdf))
242		* [A Short Study of Alexandroff Spaces]([arxiv.org](https://arxiv.org/abs/0708.2136))
	241	* Finite Topological Spaces ([www.math.uchicago.edu](https://www.math.uchicago.edu/~may/MISC/FiniteSpaces.pdf))
	242	* A Short Study of Alexandroff Spaces ([arxiv.org](https://arxiv.org/abs/0708.2136))
243	243
244	244	### Type Systems
245	245
246		* [Several types of types in programming languages]([arxiv.org](https://arxiv.org/abs/1510.03726))
247		* [Initial Algebra Semantics is Enough!]([libres.uncg.edu](https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2007_Intitial%20Algebra%20Semantics%20Is%20Enough.pdf))
248		* [Abstract Types have Existential Type]([homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf))
	246	* Several types of types in programming languages ([arxiv.org](https://arxiv.org/abs/1510.03726))
	247	* Initial Algebra Semantics is Enough! ([libres.uncg.edu](https://libres.uncg.edu/ir/asu/f/Johann_Patricia_2007_Intitial%20Algebra%20Semantics%20Is%20Enough.pdf))
	248	* Abstract Types have Existential Type ([homepages.inf.ed.ac.uk](https://homepages.inf.ed.ac.uk/gdp/publications/Abstract_existential.pdf))
249	249
250	250	### Type Theory
251	251
252	252	* [The Gentle Art of Levitation (pdf)](https://personal.cis.strath.ac.uk/conor.mcbride/levitation.pdf)
253	253	* [Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega](https://web.archive.org/web/20211207042011/http://compilers.cs.ucla.edu/popl16/)
254		* [A lean specification for GADTs: system F with first-class equality proofs]([link.springer.com](https://link.springer.com/article/10.1007/s10990-011-9065-0))
	254	* A lean specification for GADTs: system F with first-class equality proofs ([link.springer.com](https://link.springer.com/article/10.1007/s10990-011-9065-0))
255	255
256	256	### miniKanren
257	257

-5

by-rating/Valuable.md less more

26	26
27	27	### Compiler Construction
28	28
29		* [Compilers and Compiler Generators]([archive.org](https://archive.org/details/compilerscompile0000terr))
	29	* Compilers and Compiler Generators ([archive.org](https://archive.org/details/compilerscompile0000terr))
30	30
31	31	### PLDI
32	32
33		* [Theories of Programming Languages]([archive.org](https://archive.org/details/theoriesofprogra0000reyn))
	33	* Theories of Programming Languages ([archive.org](https://archive.org/details/theoriesofprogra0000reyn))
34	34
35	35	### User Interface
36	36
37		* [The Humane Interface]([archive.org](https://archive.org/details/humaneinterfacen00rask))
	37	* The Humane Interface ([archive.org](https://archive.org/details/humaneinterfacen00rask))
38	38
39	39	Valuable Papers
40	40	--------------

45	45
46	46	### Coq
47	47
48		* [Interaction Trees]([archive.org](https://archive.org/details/interaction-trees-representing-recursive-and-impure-programs-in-coq))
	48	* Interaction Trees ([archive.org](https://archive.org/details/interaction-trees-representing-recursive-and-impure-programs-in-coq))
49	49
50	50	### Equational Logic
51	51

55	55
56	56	### Formal Language
57	57
58		* [On the Structure of Context-Sensitive Grammars]([archive.org](https://archive.org/details/nasa_techdoc_19710024701))
	58	* On the Structure of Context-Sensitive Grammars ([archive.org](https://archive.org/details/nasa_techdoc_19710024701))
59	59
60	60	### Lambda Calculus
61	61

-3

scripts/build_readmes.py less more

184	184	url = onlines[0]
185	185	if url.startswith("https://en.wikipedia"):
186	186	continue
	187
	188	if url.startswith('['):
	189	link = "* {} ({})".format(entry["title"], url)
	190	else:
	191	link = "* [{}]({})".format(entry["title"], url)
	192
187	193	rating = entry["properties"].get("rating", "TODO")
188	194	if rating == target_rating:
189		selecteds.append(
190		"* [{}]({})".format(entry["title"], url)
191		)
	195	selecteds.append(link)
192	196	if selecteds:
193	197	f.write("\n### {}\n\n".format(topic))
194	198	for selected in selecteds: