From fa8bb975614b5da3eb358598a1fa379911900f0d Mon Sep 17 00:00:00 2001 From: JJ Date: Wed, 22 Nov 2023 21:49:50 -0800 Subject: meow --- computation/compilers.md | 8 +++ computation/continuations.md | 13 ++++ computation/effects.md | 1 + computation/index.md | 0 computation/modules.md | 24 ++++++++ computation/paradigms.md | 9 +++ computation/semantics.md | 1 + computation/syntax.md | 22 +++++++ computation/types.md | 11 ++++ ctf/crypto.md | 10 +++ ctf/index.md | 0 ctf/pwn.md | 7 +++ ctf/rev.md | 5 ++ ctf/web.md | 5 ++ foundations/index.md | 0 foundations/lambdas.md | 0 foundations/types.md | 0 linguistics/index.md | 0 mathematics/abstract-algebra.md | 0 mathematics/category-theory.md | 0 mathematics/coding-theory.md | 0 mathematics/complex-analysis.md | 0 mathematics/index.md | 0 mathematics/linear-algebra.md | 1 + mathematics/logic.md | 132 ++++++++++++++++++++++++++++++++++++++++ mathematics/real-analysis.md | 0 26 files changed, 249 insertions(+) create mode 100644 computation/compilers.md create mode 100644 computation/continuations.md create mode 100644 computation/effects.md create mode 100644 computation/index.md create mode 100644 computation/modules.md create mode 100644 computation/paradigms.md create mode 100644 computation/semantics.md create mode 100644 computation/syntax.md create mode 100644 computation/types.md create mode 100644 ctf/crypto.md create mode 100644 ctf/index.md create mode 100644 ctf/pwn.md create mode 100644 ctf/rev.md create mode 100644 ctf/web.md create mode 100644 foundations/index.md create mode 100644 foundations/lambdas.md create mode 100644 foundations/types.md create mode 100644 linguistics/index.md create mode 100644 mathematics/abstract-algebra.md create mode 100644 mathematics/category-theory.md create mode 100644 mathematics/coding-theory.md create mode 100644 mathematics/complex-analysis.md create mode 100644 mathematics/index.md create mode 100644 mathematics/linear-algebra.md create mode 100644 mathematics/logic.md create mode 100644 mathematics/real-analysis.md 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 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 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 diff --git a/foundations/lambdas.md b/foundations/lambdas.md new file mode 100644 index 0000000..e69de29 diff --git a/foundations/types.md b/foundations/types.md new file mode 100644 index 0000000..e69de29 diff --git a/linguistics/index.md b/linguistics/index.md new file mode 100644 index 0000000..e69de29 diff --git a/mathematics/abstract-algebra.md b/mathematics/abstract-algebra.md new file mode 100644 index 0000000..e69de29 diff --git a/mathematics/category-theory.md b/mathematics/category-theory.md new file mode 100644 index 0000000..e69de29 diff --git a/mathematics/coding-theory.md b/mathematics/coding-theory.md new file mode 100644 index 0000000..e69de29 diff --git a/mathematics/complex-analysis.md b/mathematics/complex-analysis.md new file mode 100644 index 0000000..e69de29 diff --git a/mathematics/index.md b/mathematics/index.md new file mode 100644 index 0000000..e69de29 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 -- cgit v1.2.3-70-g09d2