meow

26 files changed, 249 insertions, 0 deletions

diff --git a/computation/compilers.md b/computation/compilers.md
new file mode 100644
index 0000000..b3b1769
--- /dev/null
+++ b/computation/compilers.md
@@ -0,0 +1,8 @@
+# Compilers
+
+Books and Courses
+- [Introduction to Compiler Construction](https://www.students.cs.ubc.ca/~cs-411/2022w2/book_top.html)
+- [Programming Languages, Application and Interpretation](https://www.plai.org/)
+
+Articles
+- [Compiler Optimizations Are Hard Because They Forget](https://faultlore.com/blah/oops-that-was-important/)
diff --git a/computation/continuations.md b/computation/continuations.md
new file mode 100644
index 0000000..4d4565d
--- /dev/null
+++ b/computation/continuations.md
@@ -0,0 +1,13 @@
+# continuations
+
+## Resources
+- [nim-works CPS](https://github.com/nim-works/cps/tree/master/docs): 
+- [CPS vs. SSA](http://www.mlton.org/pipermail/mlton/2003-January/023054.html)
+- https://matt.might.net/articles/by-example-continuation-passing-style/
+- https://okmij.org/ftp/continuations/
+
+## Continuations
+
+## Continuation-passing style
+
+## Deliminated continuations
diff --git a/computation/effects.md b/computation/effects.md
new file mode 100644
index 0000000..7b8ba3e
--- /dev/null
+++ b/computation/effects.md
@@ -0,0 +1 @@
+# Effects
diff --git a/computation/index.md b/computation/index.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/computation/index.md
diff --git a/computation/modules.md b/computation/modules.md
new file mode 100644
index 0000000..8ec4b61
--- /dev/null
+++ b/computation/modules.md
@@ -0,0 +1,24 @@
+# Modules
+
+An overarching question I've had that I've been unable to resolve: are ML-style modules any more expressive than a system with:
+- polymorphic data types
+- polymorphic interface types
+- first-class modules, that are *not* polymorphic (no functors)?
+
+## Resources
+
+Papers
+- [F-ing Modules](https://www.cambridge.org/core/journals/journal-of-functional-programming/article/fing-modules/B573FA00832D55D4878863DE1725D90B) (2014)
+
+Posts
+- [Modules Matter Most](https://existentialtype.wordpress.com/2011/04/16/modules-matter-most/)
+  - [Modules Matter Most (presentation)](http://macqueenfest.cs.uchicago.edu/slides/harper.pdf)
+- ['Modules Matter Most' for the Masses](https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html)
+- [First-Class Modules: An Introduction](https://dev.realworldocaml.org/first-class-modules.html)
+- [Exotic Programming Ideas: Module Systems](https://www.stephendiehl.com/posts/exotic01.html)
+- [A Crash Course on ML Modules](https://jozefg.bitbucket.io/posts/2015-01-08-modules.html)
+- [UW CSE 341: ML Modules](https://courses.cs.washington.edu/courses/cse341/04wi/lectures/09-ml-modules.html)
+
+Books
+- [ATTAPL Ch. 8: Design Considerations for ML-style Module Systems]()
+
diff --git a/computation/paradigms.md b/computation/paradigms.md
new file mode 100644
index 0000000..59261ae
--- /dev/null
+++ b/computation/paradigms.md
@@ -0,0 +1,9 @@
+# Programming Paradigms
+
+## Imperative Programming
+
+## Object-Oriented Programming
+
+## Functional Programming
+
+...
diff --git a/computation/semantics.md b/computation/semantics.md
new file mode 100644
index 0000000..e3e063a
--- /dev/null
+++ b/computation/semantics.md
@@ -0,0 +1 @@
+# Formal Semantics
diff --git a/computation/syntax.md b/computation/syntax.md
new file mode 100644
index 0000000..7dd776d
--- /dev/null
+++ b/computation/syntax.md
@@ -0,0 +1,22 @@
+# Syntax
+
+## Resources
+
+Articles
+- [An Overview of Lexing and Parsing](https://www.perl.com/pub/2012/10/an-overview-of-lexing-and-parsing.html/)
+- [Just write the #!%/* parser](https://tiarkrompf.github.io/notes/?/just-write-the-parser/)
+
+Books and Courses
+- [Compilers: Principles, Techniques, Tools](https://annas-archive.org/md5/90db32d070cfb70ca617e655d5c35529)
+
+## Notation
+
+## Lexing
+
+## Parsing
+
+cover:
+- please please please lex
+- handrolled parsers
+- pegs and their limitations
+- other varieties of parser generators (ANTLR, lalrpop, yacc...)
diff --git a/computation/types.md b/computation/types.md
new file mode 100644
index 0000000..2edfe7c
--- /dev/null
+++ b/computation/types.md
@@ -0,0 +1,11 @@
+# types! ah, wonderous types!
+
+## Resources
+
+- *Types and Programming Languages* by Benjamin C. Pierce
+
+## algebraic data types
+
+## inductive types
+- https://en.wikipedia.org/wiki/Inductive_type
+
diff --git a/ctf/crypto.md b/ctf/crypto.md
new file mode 100644
index 0000000..a1d645c
--- /dev/null
+++ b/ctf/crypto.md
@@ -0,0 +1,10 @@
+# Cryptography for Computer Security
+
+## Resources
+
+- [Cryptohack](https://cryptohack.com)
+- [Cryptopals](https://cryptopals.org)
+
+## Notes on Cryptohack
+
+## Notes on Cryptopals
diff --git a/ctf/index.md b/ctf/index.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/ctf/index.md
diff --git a/ctf/pwn.md b/ctf/pwn.md
new file mode 100644
index 0000000..ed75eea
--- /dev/null
+++ b/ctf/pwn.md
@@ -0,0 +1,7 @@
+# Binary Exploitation
+
+## Resources
+
+- [pwn.college](https://pwn.college)
+- [pwnable.kr](https://pwnable.kr/)
+- [how2heap](https://github.com/shellphish/how2heap)
diff --git a/ctf/rev.md b/ctf/rev.md
new file mode 100644
index 0000000..a4bfc1d
--- /dev/null
+++ b/ctf/rev.md
@@ -0,0 +1,5 @@
+# Reverse Engineering
+
+## Resources
+
+- [crackmes.one](https://crackmes.one)
diff --git a/ctf/web.md b/ctf/web.md
new file mode 100644
index 0000000..3e40a62
--- /dev/null
+++ b/ctf/web.md
@@ -0,0 +1,5 @@
+# Web Security
+
+## Resources
+
+- [websec.fr](https://websec.fr)
diff --git a/foundations/index.md b/foundations/index.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/foundations/index.md
diff --git a/foundations/lambdas.md b/foundations/lambdas.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/foundations/lambdas.md
diff --git a/foundations/types.md b/foundations/types.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/foundations/types.md
diff --git a/linguistics/index.md b/linguistics/index.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/linguistics/index.md
diff --git a/mathematics/abstract-algebra.md b/mathematics/abstract-algebra.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/mathematics/abstract-algebra.md
diff --git a/mathematics/category-theory.md b/mathematics/category-theory.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/mathematics/category-theory.md
diff --git a/mathematics/coding-theory.md b/mathematics/coding-theory.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/mathematics/coding-theory.md
diff --git a/mathematics/complex-analysis.md b/mathematics/complex-analysis.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/mathematics/complex-analysis.md
diff --git a/mathematics/index.md b/mathematics/index.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/mathematics/index.md
diff --git a/mathematics/linear-algebra.md b/mathematics/linear-algebra.md
new file mode 100644
index 0000000..fbd4a63
--- /dev/null
+++ b/mathematics/linear-algebra.md
@@ -0,0 +1 @@
+# Linear Algebra
diff --git a/mathematics/logic.md b/mathematics/logic.md
new file mode 100644
index 0000000..8068751
--- /dev/null
+++ b/mathematics/logic.md
@@ -0,0 +1,132 @@
+# sparse notes on logic, mathematics, and that around and in between
+
+## kinds of logic
+
+there are different types of logic!
+
+some such systems:
+- classical logic
+- intuitionistic logic
+- paraconsistent logic
+
+and many others.
+
+## orders of logic
+
+### [propositional logic](https://ncatlab.org/nlab/show/propositional+logic)
+
+**propositional logic** or *0th-order logic* deals with raw *propositions*.
+**propositions** are statements that *reduce* to a **truth value**.
+truth values are classically either true or false. i'm not quite sure if there are alternative approaches that change this.
+
+the basic foundations of propositional logic are as follows:
+------|--------------
+p     | a proposition
+¬p    | not p
+p → q | p implies q
+⊤     | true
+⊥     | false
+⊢     | derives/yields
+
+several logical concepts are *derivable* from the above:
+------|--------------------|----
+p ∨ q | ¬p → q             | or
+p ∧ q | ¬(p → ¬q)          | and
+p ⟺ q | (p → q) ∧ (q → p)  | iff
+p ⊕ q | (p ∨ q) ∧ ¬(p ∧ q) | xor
+
+to do anything interesting, several rules must exist:
+
+replacement rules
+------------------------------------|----------------
+((p ∨ q) ∨ r) → (p ∨ (q ∨ r))       | associative
+(p ∧ q) → (q ∧ p)                   | commutative
+((p ∧ q) → r) → (p → (q → r))       | exportation
+(p → q) → (¬q → ¬p)                 | transposition
+(p → q) → (¬p ∨ q)                  | implication
+((p ∨ q) ∨ r) → ((p ∧ r) ∨ (q ∧ r)) | distributive
+((p) ∧ (q)) → (p ∧ q)               | conjunction
+p ⟺ (¬¬p)                           | double negation
+
+double negation is not allowed in intuistionistic logic systems.
+
+### [predicate logic](https://ncatlab.org/nlab/show/predicate+logic)
+
+**predicate logic** or *first-order logic* adds variables and quantifiers to propositions:
+* ∀x: for all x
+* ∃y: there exists a y
+
+these additions are enough to serve as a foundation of mathematics...
+
+## philosophy of mathematics
+
+what mathematics *is* is not universally agreed upon.
+
+there are two primary
+
+
+logicism is generally widely regarded as correct
+
+these philosophies
+
+there are others, but none that i am interested in.
+
+## foundations of mathematics
+
+### set theory
+
+there have been a number of set theories, of varying consistency
+
+
+naive set theory was shown inconsistent
+
+
+### type theory
+
+*type theories* can serve as an alternative (equivalent) foundation of mathematics.
+
+
+but what is the point in fashioning equivalent foundations when standard ZFC works just fine?
+
+an alternative (equivalent) foundation of mathematics are *type theories*.
+
+
+## the curry-howard correspondence
+
+the **curry-howard correspondence** or *propositions-as-types*
+
+
+symbol | logic | types
+---|-------------|--------------
+⊤  | true        | top type
+⊥  | false       | bottom type
+→  | implication | function type
+∧  | conjunction | product type
+∨  | disjunction | sum type
+∀  | universal   | dependent product type
+∃  | existential | dependent sum type
+
+a couple of other notes.
+programs as proofs comes into play when 
+you MUST have a constructed thing with a type
+
+no negation??
+don't fully understand the distinction between dependent and nondependent types
+implication over types?
+
+
+
+## [principle of explosion](https://en.wikipedia.org/wiki/Principle_of_explosion)
+
+what's wrong with inconsistency, anyway?
+
+it may or may not be intuitive that a contradiction can lead to further contradictions.
+either way, an example can be helpful.
+the following logic proves any arbitrary statement B:
+
+```logic
+A = ⊤, ¬A = ⊤
+A ∨ B = ⊤
+¬A ⇒ A = ⊥
+⊥ ∨ B ⇒ B = ⊤
+```
diff --git a/mathematics/real-analysis.md b/mathematics/real-analysis.md
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/mathematics/real-analysis.md