Commit c16c091188a126b3b2a060625499e25e98915a48 - The-Glosscubator

+1

-3

Lambda Calculus/src/Books.md less more

14	14	* online @ [archive.org](https://archive.org/details/AnnalsOfMathematicalStudies6ChurchAlonzoTheCalculiOfLambdaConversionPrincetonUniversityPress1941)
15	15	* online @ [archive.org](https://archive.org/details/the-calculi-of-lambda-conversion-couverture-alonzo-church-princeton-university-p)
16	16	* excerpt @ [www.jfsowa.com](http://www.jfsowa.com/logic/alonzo.htm)
17		* rating: classic
18	17
19	18	Alonzo Church's 1941 exposition of the lambda calculus.
20	19

23	22	* author: J. Roger Hindley, Jonathan P. Seldin
24	23	* date: 1986
25	24	* borrow @ [archive.org](https://archive.org/details/introductiontoco0000hind)
26		* rating: TODO
27	25
28		Barendregt 1984 should be on this list but isn't. So, this is.
	26	.

+0

-6

Lambda Calculus/src/Papers.md less more

11	11	* authors: Achim Jung
12	12	* date: 2004
13	13	* url: https://www.cs.bham.ac.uk/~axj/pub/papers/lambda-calculus.pdf
14		* rating: 2
15	14
16	15	.
17	16

20	19	* authors: Henk Barendregt, Erik Barendsen
21	20	* date: December 1998, March 2000
22	21	* url: https://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf
23		* rating: 2
24	22
25	23	.
26	24
27	25	### Chapter 5: The Untyped Lambda Calculus (slides) (pdf)
28	26
29	27	* url: https://xiongyingfei.github.io/DPPL/2021/xiong_ch5.pdf
30		* rating: 2
31	28
32	29	.
33	30
34	31	### Untyped Lambda Calculus (slides) (pdf)
35	32
36	33	* url: https://www3.cs.stonybrook.edu/~cram/cse526/Spring20/Lectures/untyped-lambda.pdf
37		* rating: 1
38	34
39	35	.
40	36
41	37	### A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure - CORE Reader
42	38
43	39	* url: https://core.ac.uk/reader/47112580
44		* rating: 1
45	40
46	41	.
47	42

52	47	* publisher: https://dl.acm.org/doi/10.1017/S0956796801004294
53	48	* online @ [www.mscs.dal.ca](https://www.mscs.dal.ca/~selinger/papers/combinatory.pdf)
54	49	* topics: Lambda Calculus, Algebraic Logic
55		* rating: 3
56	50
57	51	.
58	52

+0

-7

Lambda Calculus/src/Webpages.md less more

9	9	### functional programming - Is Lambda Calculus purely syntactic? - Computer Science Stack Exchange
10	10
11	11	* url: https://cs.stackexchange.com/questions/110375/is-lambda-calculus-purely-syntactic
12		* rating: 1
13	12
14	13	.
15	14
16	15	### What are the axioms, inference rules, and (formal) semantics of lambda calculus? - Computer Science Stack Exchange
17	16
18	17	* url: https://cs.stackexchange.com/questions/28452/what-are-the-axioms-inference-rules-and-formal-semantics-of-lambda-calculus
19		* rating: 1
20	18
21	19	.
22	20
23	21	### lo.logic - What\'s the point of \$\\eta\$-conversion in lambda calculus? - Theoretical Computer Science Stack Exchange
24	22
25	23	* url: https://cstheory.stackexchange.com/questions/8259/whats-the-point-of-eta-conversion-in-lambda-calculus
26		* rating: 1
27	24
28	25	.
29	26
30	27	### lambda calculus - What\'s the definition of equational theory? Why is λ logic free? - Mathematics Stack Exchange
31	28
32	29	* url: https://math.stackexchange.com/questions/802494/whats-the-definition-of-equational-theory-why-is-%CE%BB-logic-free
33		* rating: 1
34	30
35	31	.
36	32
37	33	### lo.logic - Scott on the consistency of the lambda calculus - MathOverflow
38	34
39	35	* url: https://mathoverflow.net/questions/16752/scott-on-the-consistency-of-the-lambda-calculus
40		* rating: 1
41	36
42	37	.
43	38

50	45	### The largest number representable in 64 bits
51	46
52	47	* url: https://tromp.github.io/blog/2023/11/24/largest-number
53		* rating: 1
54	48
55	49	.
56	50
57	51	### lo.logic - What\'t the smallest lambda calculus term which is not known to have a normal form? - MathOverflow
58	52
59	53	* url: https://mathoverflow.net/questions/353514/whatt-the-smallest-lambda-calculus-term-which-is-not-known-to-have-a-normal-for
60		* rating: 1
61	54
62	55	.
63	56

+111

-0

Lambda Calculus/src/commentary/Chris Pressey.md less more

	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	Lambda Calculus
	13	---------------
	14
	15	### The Calculi of Lambda-Conversion
	16
	17	* rating: classic
	18
	19	.
	20
	21	### Introduction to Combinators and the Lambda Calculus
	22
	23	* rating: TODO
	24
	25	Barendregt 1984 should be on this list but isn't. So, this is.
	26
	27	### A Short Introduction to the Lambda Calculus
	28
	29	* rating: 2
	30
	31	.
	32
	33	### Introduction to Lambda Calculus
	34
	35	* rating: 2
	36
	37	.
	38
	39	### Chapter 5: The Untyped Lambda Calculus (slides) (pdf)
	40
	41	* rating: 2
	42
	43	.
	44
	45	### Untyped Lambda Calculus (slides) (pdf)
	46
	47	* rating: 1
	48
	49	.
	50
	51	### A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure - CORE Reader
	52
	53	* rating: 1
	54
	55	.
	56
	57	### The Lambda Calculus is Algebraic
	58
	59	* rating: 3
	60
	61	.
	62
	63	### functional programming - Is Lambda Calculus purely syntactic? - Computer Science Stack Exchange
	64
	65	* rating: 1
	66
	67	.
	68
	69	### What are the axioms, inference rules, and (formal) semantics of lambda calculus? - Computer Science Stack Exchange
	70
	71	* rating: 1
	72
	73	.
	74
	75	### lo.logic - What\'s the point of \$\\eta\$-conversion in lambda calculus? - Theoretical Computer Science Stack Exchange
	76
	77	* rating: 1
	78
	79	.
	80
	81	### lambda calculus - What\'s the definition of equational theory? Why is λ logic free? - Mathematics Stack Exchange
	82
	83	* rating: 1
	84
	85	.
	86
	87	### lo.logic - Scott on the consistency of the lambda calculus - MathOverflow
	88
	89	* rating: 1
	90
	91	.
	92
	93	### Lambda Terms
	94
	95	* rating: TODO
	96
	97	.
	98
	99	### The largest number representable in 64 bits
	100
	101	* rating: 1
	102
	103	.
	104
	105	### lo.logic - What\'t the smallest lambda calculus term which is not known to have a normal form? - MathOverflow
	106
	107	* rating: 1
	108
	109	.
	110

+0

-6

Linguistics/src/Books.md less more

11	11	* author: Terence D. Langendoen
12	12	* date: 1970
13	13	* borrow @ [archive.org](https://archive.org/details/essentialsofengl0000lang)
14		* rating: 1
15	14
16	15	.
17	16

20	19	* author: Roderick Jacobs
21	20	* date: 1970
22	21	* borrow @ [archive.org](https://archive.org/details/englishtransform0000jaco_p1k5)
23		* rating: 1
24	22
25	23	.
26	24

29	27	* author: John P. Broderick
30	28	* date: 1975
31	29	* borrow @ [archive.org](https://archive.org/details/modernenglishlin0000brod)
32		* rating: 1
33	30
34	31	.
35	32

38	35	* author: Geoffrey N. Leech
39	36	* date: 1970
40	37	* borrow @ [archive.org](https://archive.org/details/towardssemanticd0000leec)
41		* rating: 1
42	38
43	39	.
44	40

49	45	* borrow @ [archive.org](https://archive.org/details/introductiontoun00shie)
50	46	* online @ [dash.harvard.edu](https://dash.harvard.edu/bitstream/handle/1/11576719/shieber-uagf-distrib-130816_0.pdf)
51	47	* topics: Linguistics, Formal Language, Unification
52		* rating: 1
53	48
54	49	The PDF is CC-BY-3.0-unported.
55	50

59	54	* date: 1993
60	55	* borrow @ [archive.org](https://archive.org/details/languagecomplexi00rist)
61	56	* topics: Linguistics, Computational Complexity
62		* rating: 1
63	57
64	58	.

+0

-1

Linguistics/src/Webpages.md less more

9	9	### ACL Anthology - ACL Anthology
10	10
11	11	* url: https://aclanthology.org/
12		* rating: 1
13	12
14	13	.

+57

-0

Linguistics/src/commentary/Chris Pressey.md less more

	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	Linguistics
	13	---------------
	14
	15	### Essentials of English Grammar
	16
	17	* rating: 1
	18
	19	.
	20
	21	### English Transformational Grammar
	22
	23	* rating: 1
	24
	25	.
	26
	27	### Modern English Linguistics
	28
	29	* rating: 1
	30
	31	.
	32
	33	### Towards a Semantic Description of English
	34
	35	* rating: 1
	36
	37	.
	38
	39	### An Introduction to Unification-based Approaches to Grammar
	40
	41	* rating: 1
	42
	43	.
	44
	45	### The Language Complexity Game
	46
	47	* rating: 1
	48
	49	.
	50
	51	### ACL Anthology - ACL Anthology
	52
	53	* rating: 1
	54
	55	.
	56

+0

-4

Lisp/src/Books.md less more

12	12	* date: 1962
13	13	* borrow @ [archive.org](https://archive.org/details/lisp15programmer00john)
14	14	* online @ [archive.org](https://archive.org/details/DTIC_AD0406138)
15		* rating: classic
16	15
17	16	Has some classics in it, like a Wang theorem prover.
18	17

21	20	* authors: Daniel P. Friedman
22	21	* date: 1974
23	22	* online @ [archive.org](https://archive.org/details/tlLISP)
24		* rating: classic
25	23
26	24	.
27	25

32	30	* online @ [archive.org](https://archive.org/details/lisp-1981-addison-wesley)
33	31	* borrow @ [archive.org](https://archive.org/details/lisp1989wins)
34	32	* borrow @ [archive.org](https://archive.org/details/lispwins00wins)
35		* rating: 1
36	33
37	34	.
38	35

41	38	* author: John H Riely
42	39	* date: 1992
43	40	* borrow @ [archive.org](https://archive.org/details/commonlispworkbo0000rile)
44		* rating: 0
45	41
46	42	.

+0

-2

Lisp/src/Webpages.md less more

9	9	### The Standard Lisp Report
10	10
11	11	* url: http://www.reduce-algebra.com/lisp-docs/
12		* rating: 1
13	12
14	13	.
15	14
16	15	### clojure - What are the tasks of the "reader" during Lisp interpretation? - Stack Overflow
17	16
18	17	* url: https://stackoverflow.com/questions/4537793/what-are-the-tasks-of-the-reader-during-lisp-interpretation
19		* rating: 1
20	18
21	19	.
22	20

+51

-0

Lisp/src/commentary/Chris Pressey.md less more

	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	Lisp
	13	---------------
	14
	15	### Lisp 1.5 Programmer's Manual
	16
	17	* rating: classic
	18
	19	.
	20
	21	### The Little Lisper
	22
	23	* rating: classic
	24
	25	.
	26
	27	### Lisp
	28
	29	* rating: 1
	30
	31	.
	32
	33	### A Common Lisp Workbook
	34
	35	* rating: 0
	36
	37	.
	38
	39	### The Standard Lisp Report
	40
	41	* rating: 1
	42
	43	.
	44
	45	### clojure - What are the tasks of the "reader" during Lisp interpretation? - Stack Overflow
	46
	47	* rating: 1
	48
	49	.
	50

+0

-1

Logic Programming/src/Books.md less more

11	11	* author: Dale Miller
12	12	* date: 2012
13	13	* borrow @ [archive.org](https://archive.org/details/programmingwithh0000mill)
14		* rating: TODO
15	14
16	15	LambdaProlog and HOAS.

+0

-1

Logic Programming/src/Papers.md less more

11	11	* authors: van Emden, Robert Kowalski
12	12	* date: 1976
13	13	* online @ [doc.ic.ac.uk](https://www.doc.ic.ac.uk/~rak/papers/kowalski-van_emden.pdf)
14		* rating: classic
15	14
16	15	.

+0

-3

Logic Programming/src/Webpages.md less more

9	9	### prolog - What are the best uses of Logic Programming? - Stack Overflow
10	10
11	11	* url: https://stackoverflow.com/questions/215742/what-are-the-best-uses-of-logic-programming
12		* rating: 1
13	12
14	13	.
15	14
16	15	### prolog - How to implement fully-declarative Horn logic? - Stack Overflow
17	16
18	17	* url: https://stackoverflow.com/questions/31674831/how-to-implement-fully-declarative-horn-logic
19		* rating: 1
20	18
21	19	.
22	20
23	21	### Dept. of Computing, Imperial College, London: Robert Kowalski Home Page
24	22
25	23	* url: https://www.doc.ic.ac.uk/~rak/
26		* rating: 1
27	24
28	25	.
29	26

+45

-0

Logic Programming/src/commentary/Chris Pressey.md less more

	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	Logic Programming
	13	---------------
	14
	15	### Programming with Higher-Order Logic
	16
	17	* rating: TODO
	18
	19	.
	20
	21	### The Semantics of Predicate Logic as a Programming Language
	22
	23	* rating: classic
	24
	25	.
	26
	27	### prolog - What are the best uses of Logic Programming? - Stack Overflow
	28
	29	* rating: 1
	30
	31	.
	32
	33	### prolog - How to implement fully-declarative Horn logic? - Stack Overflow
	34
	35	* rating: 1
	36
	37	.
	38
	39	### Dept. of Computing, Imperial College, London: Robert Kowalski Home Page
	40
	41	* rating: 1
	42
	43	.
	44

+1

-1

Lua/src/Webpages.md less more

10	10
11	11	* url: https://lua.org/
12	12
13		future-rating: 2.5 useful
	13	.
14	14
15	15	### Lua 5.3.5 Online Demo for MS-DOS : Lua.org, PUC-Rio : Free Download, Borrow, and Streaming : Internet Archive
16	16

+1

-1

Lua/src/commentary/Chris Pressey.md less more

16	16
17	17	* rating: 2
18	18
19		.
	19	future-rating: 2.5 useful
20	20
21	21	### The Programming Language Lua
22	22

+1

-2

Model Checking/src/Repositories.md less more

10	10
11	11	* url: https://github.com/tlaplus/PlusPy
12	12	* license: MIT
13		* rating: 2
14	13
15		This is not actually model checking, this is interpreting TLA+.
	14	.

+0

-7

Model Checking/src/Webpages.md less more

15	15	### Lecture Notes on CTL Model Checking - 23-ctl.pdf
16	16
17	17	* url: https://www.cs.cmu.edu/~15414/s23/s22/lectures/23-ctl.pdf
18		* rating: 1
19	18
20	19	.
21	20

28	27	### The TLA+ Home Page
29	28
30	29	* url: https://lamport.azurewebsites.net/tla/tla.html
31		* rating: 1
32	30
33	31	.
34	32
35	33	### Learn TLA+ --- Learn TLA+
36	34
37	35	* url: https://www.learntla.com/
38		* rating: 1
39	36
40	37	.
41	38
42	39	### Practical TLA+ by Hillel Wayne
43	40
44	41	* url: https://lamport.azurewebsites.net/tla/practical-tla.html
45		* rating: 1
46	42
47	43	.
48	44

55	51	### Alloy (specification language) - Wikipedia
56	52
57	53	* url: https://en.wikipedia.org/wiki/Alloy_(specification_language)
58		* rating: 1
59	54
60	55	.
61	56
62	57	### multi tasking - Help understanding Petersons Algorithm for N Processes - Computer Science Stack Exchange
63	58
64	59	* url: https://cs.stackexchange.com/questions/164777/help-understanding-petersons-algorithm-for-n-processes
65		* rating: 1
66	60
67	61	future-topics: Promela
68	62

70	64
71	65	* url: https://sri-csl.github.io/sally/
72	66	* associated-repo-url: https://github.com/SRI-CSL/sally
73		* rating: 1
74	67
75	68	.

+48

-0

Model Checking/src/commentary/Chris Pressey.md less more

32	32	* rating: TODO
33	33
34	34	.
	35
	36	### Lecture Notes on CTL Model Checking - 23-ctl.pdf
	37
	38	* rating: 1
	39
	40	.
	41
	42	### The TLA+ Home Page
	43
	44	* rating: 1
	45
	46	.
	47
	48	### Learn TLA+ --- Learn TLA+
	49
	50	* rating: 1
	51
	52	.
	53
	54	### Practical TLA+ by Hillel Wayne
	55
	56	* rating: 1
	57
	58	.
	59
	60	### Alloy (specification language) - Wikipedia
	61
	62	* rating: 1
	63
	64	.
	65
	66	### multi tasking - Help understanding Petersons Algorithm for N Processes - Computer Science Stack Exchange
	67
	68	* rating: 1
	69
	70	The answerer gives a Promela model for the algorithm
	71
	72	### Sally by SRI-CSL
	73
	74	* rating: 1
	75
	76	.
	77
	78	### tlaplus/PlusPy: Python interpreter for TLA+ specifications
	79
	80	* rating: 2
	81
	82	This is not actually model checking, this is interpreting TLA+.