From 439c5d3ef5fb8b8ebba28d45088d9b91db7418ac Mon Sep 17 00:00:00 2001 From: JJ Date: Thu, 4 Jan 2024 18:37:28 -0800 Subject: meow --- _layouts/computation.html | 18 +-- _layouts/ctf.html | 6 +- _layouts/plt.html | 41 +++++++ _layouts/web.html | 31 ++++++ computation/compilers.md | 15 --- computation/continuations.md | 19 ---- computation/effects.md | 27 ----- computation/lambda-calculus.md | 6 - computation/memory-management.md | 21 ---- computation/modules.md | 28 ----- computation/monads.md | 8 -- computation/networking.md | 12 -- computation/paradigms.md | 14 --- computation/patterns.md | 6 - computation/semantics.md | 8 -- computation/syntax.md | 29 ----- computation/types.md | 50 --------- ctf/crypto.md | 5 +- ctf/pwn.md | 2 +- ctf/rev.md | 2 +- ctf/web.md | 2 +- plt/compilers.md | 15 +++ plt/continuations.md | 19 ++++ plt/effects.md | 27 +++++ plt/lambda-calculus.md | 6 + plt/memory-management.md | 21 ++++ plt/modules.md | 25 +++++ plt/monads.md | 8 ++ plt/paradigms.md | 14 +++ plt/patterns.md | 6 + plt/pragmatics.md | 12 ++ plt/semantics.md | 8 ++ plt/syntax.md | 29 +++++ plt/types.md | 50 +++++++++ web/css.md | 234 +++++++++++++++++++++++++++++++++++++++ web/html.md | 217 ++++++++++++++++++++++++++++++++++++ web/htmx.md | 12 ++ web/index.md | 5 + web/networking.md | 12 ++ web/tailwind.md | 12 ++ web/wasm.md | 5 + 41 files changed, 822 insertions(+), 265 deletions(-) create mode 100644 _layouts/plt.html create mode 100644 _layouts/web.html delete mode 100644 computation/compilers.md delete mode 100644 computation/continuations.md delete mode 100644 computation/effects.md delete mode 100644 computation/lambda-calculus.md delete mode 100644 computation/memory-management.md delete mode 100644 computation/modules.md delete mode 100644 computation/monads.md delete mode 100644 computation/networking.md delete mode 100644 computation/paradigms.md delete mode 100644 computation/patterns.md delete mode 100644 computation/semantics.md delete mode 100644 computation/syntax.md delete mode 100644 computation/types.md create mode 100644 plt/compilers.md create mode 100644 plt/continuations.md create mode 100644 plt/effects.md create mode 100644 plt/lambda-calculus.md create mode 100644 plt/memory-management.md create mode 100644 plt/modules.md create mode 100644 plt/monads.md create mode 100644 plt/paradigms.md create mode 100644 plt/patterns.md create mode 100644 plt/pragmatics.md create mode 100644 plt/semantics.md create mode 100644 plt/syntax.md create mode 100644 plt/types.md create mode 100644 web/css.md create mode 100644 web/html.md create mode 100644 web/htmx.md create mode 100644 web/index.md create mode 100644 web/networking.md create mode 100644 web/tailwind.md create mode 100644 web/wasm.md diff --git a/_layouts/computation.html b/_layouts/computation.html index e4b54db..094ef31 100644 --- a/_layouts/computation.html +++ b/_layouts/computation.html @@ -10,23 +10,11 @@ layout: default mathematics linguistics computation - ctf diff --git a/_layouts/ctf.html b/_layouts/ctf.html index bd9b2dd..0286880 100644 --- a/_layouts/ctf.html +++ b/_layouts/ctf.html @@ -9,8 +9,12 @@ layout: default +

rev diff --git a/_layouts/plt.html b/_layouts/plt.html new file mode 100644 index 0000000..463950c --- /dev/null +++ b/_layouts/plt.html @@ -0,0 +1,41 @@ +--- +layout: default +--- +

+ apropos +

+ + + +

+{{ content }} +

diff --git a/_layouts/web.html b/_layouts/web.html new file mode 100644 index 0000000..2079d24 --- /dev/null +++ b/_layouts/web.html @@ -0,0 +1,31 @@ +--- +layout: default +--- +

+ apropos +

+ + + +

+{{ content }} +

diff --git a/computation/compilers.md b/computation/compilers.md deleted file mode 100644 index 8e6ebbf..0000000 --- a/computation/compilers.md +++ /dev/null @@ -1,15 +0,0 @@ ---- -layout: computation -title: computation/compilers ---- - -# compilers - -articles -- [Compiler optimizations are hard because they forget](https://faultlore.com/blah/oops-that-was-important/) -- [A tutorial on how to write a compiler using LLVM](https://tomassetti.me/a-tutorial-on-how-to-write-a-compiler-using-llvm/) - -books and courses -- [Programming Languages, Application and Interpretation](https://www.plai.org/) -- [Introduction to Compiler Construction](https://www.students.cs.ubc.ca/~cs-411/2022w2/book_top.html) -- [Design Your Own Language (book list)](https://slebok.github.io/dyol/books/index.html) diff --git a/computation/continuations.md b/computation/continuations.md deleted file mode 100644 index 08017c5..0000000 --- a/computation/continuations.md +++ /dev/null @@ -1,19 +0,0 @@ ---- -layout: computation -title: computation/continuations ---- - -# continuations - -- [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) -- [By example: continuation-passing style](https://matt.might.net/articles/by-example-continuation-passing-style/) -- [How to compile with continuations](https://matt.might.net/articles/cps-conversion/) -- [**Oleg Kiselyov's writings**](https://okmij.org/ftp/continuations/) -- [An argument against call/cc](https://okmij.org/ftp/continuations/against-callcc.html) - -## continuations - -## continuation-passing style - -## deliminated continuations diff --git a/computation/effects.md b/computation/effects.md deleted file mode 100644 index 17c558d..0000000 --- a/computation/effects.md +++ /dev/null @@ -1,27 +0,0 @@ ---- -layout: computation -title: computation/effects ---- - -# effects - -posts -- [Oleg Kiselyov's writings](https://www.okmij.org/ftp/) -- [Exotic Programming Ideas: Effect Systems](https://www.stephendiehl.com/posts/exotic03.html) -- [Faking algebraic effects and handlers with traits](https://blog.shtsoft.eu/2022/12/22/effect-trait-dp.html) -- [From deliminated continuations to algebraic effects](https://blog.poisson.chat/posts/2023-01-02-del-cont-examples.html) -- [OCaml effects tutorial](https://github.com/ocaml-multicore/ocaml-effects-tutorial) -- [Simple functional effects with tag unions](https://www.youtube.com/watch?v=7SidSvJcPd0) -- [Effect bibliography](https://github.com/yallop/effects-bibliography) - -papers -- [What is algebraic about algebraic effects and handlers?](https://arxiv.org/abs/1807.05923) -- [Asynchronous effects](https://dl.acm.org/doi/10.1145/3434305) - -languages -- [Koka](https://koka-lang.github.io/koka/doc/book.html) -- [Effekt](https://effekt-lang.org/) -- [Eff](https://www.eff-lang.org/) -- [Unison](https://www.unison-lang.org/) -- [Effect handlers for WebAssembly](https://wasmfx.dev/) -- [Coeffects: Context-aware programming languages](https://tomasp.net/coeffects/) diff --git a/computation/lambda-calculus.md b/computation/lambda-calculus.md deleted file mode 100644 index 78752db..0000000 --- a/computation/lambda-calculus.md +++ /dev/null @@ -1,6 +0,0 @@ ---- -layout: computation -title: computation/lambda calculus ---- - -# the lambda calculus diff --git a/computation/memory-management.md b/computation/memory-management.md deleted file mode 100644 index a2edadc..0000000 --- a/computation/memory-management.md +++ /dev/null @@ -1,21 +0,0 @@ ---- -layout: computation -title: computation/memory management ---- - -# memory management - -lobster -- [Memory Management in Lobster](https://aardappel.github.io/lobster/memory_management.html) - -nim -- [ARC/ORC in Nim](https://nim-lang.org/blog/2020/10/15/introduction-to-arc-orc-in-nim.html) -- [ORC in Nim](https://nim-lang.org/blog/2020/12/08/introducing-orc.html) -- [Destructors and Move Semantics in Nim](https://nim-lang.org/docs/destructors.html) -- [Nim's ARC/ORC and Rust's move semantics](https://paste.sr.ht/blob/731278535144f00fb0ecfc41d6ee48513233baa4) - -## reference counting - -## tracing - -## ownership diff --git a/computation/modules.md b/computation/modules.md deleted file mode 100644 index be7b7e5..0000000 --- a/computation/modules.md +++ /dev/null @@ -1,28 +0,0 @@ ---- -layout: computation -title: computation/modules ---- - -# 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/) (and [slides](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](https://annas-archive.org/md5/7175434efd5620b4b117aa45a01777fa) - diff --git a/computation/monads.md b/computation/monads.md deleted file mode 100644 index c6cc0da..0000000 --- a/computation/monads.md +++ /dev/null @@ -1,8 +0,0 @@ ---- -layout: computation -title: computation/monads ---- - -# monads - -- [Monads in 300 words](https://lambda.xyz/blog/monads/) diff --git a/computation/networking.md b/computation/networking.md deleted file mode 100644 index a47eee6..0000000 --- a/computation/networking.md +++ /dev/null @@ -1,12 +0,0 @@ ---- -layout: computation -title: computation/networking ---- - -# the networking layer of the internet - -## routing: IP, DNS - -## transport: TCP, UDP, QUIC - -## content: HTTP, FTP diff --git a/computation/paradigms.md b/computation/paradigms.md deleted file mode 100644 index 198a522..0000000 --- a/computation/paradigms.md +++ /dev/null @@ -1,14 +0,0 @@ ---- -layout: computation -title: computation/programming paradigms ---- - -# reflections on programming paradigms - -## imperative programming - -## object-oriented programming - -## functional programming - -... diff --git a/computation/patterns.md b/computation/patterns.md deleted file mode 100644 index 6236411..0000000 --- a/computation/patterns.md +++ /dev/null @@ -1,6 +0,0 @@ ---- -layout: computation -title: computation/design patterns ---- - -# ways of going about doing things diff --git a/computation/semantics.md b/computation/semantics.md deleted file mode 100644 index 410d0ef..0000000 --- a/computation/semantics.md +++ /dev/null @@ -1,8 +0,0 @@ ---- -layout: computation -title: computation/semantics ---- - -# formal semantics - -## denotational semantics diff --git a/computation/syntax.md b/computation/syntax.md deleted file mode 100644 index 31b95a5..0000000 --- a/computation/syntax.md +++ /dev/null @@ -1,29 +0,0 @@ ---- -layout: computation -title: computation/syntax ---- - -# syntax - -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 -- [_Compilers: Principles, Techniques, Tools_](https://annas-archive.org/md5/90db32d070cfb70ca617e655d5c35529) - -## notation - -ebnf - -npegs - -## 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 deleted file mode 100644 index 18bc9d2..0000000 --- a/computation/types.md +++ /dev/null @@ -1,50 +0,0 @@ ---- -layout: computation -title: computation/types ---- - -# types! ah, wonderous types! - -posts -- ✨ [**How should I read type system notation?**](https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/) -- [Programming Language Theory resources](https://steshaw.org/plt/) - -books -- ✨ [_**Types and Programming Languages**_](https://www.cis.upenn.edu/~bcpierce/tapl/) by Benjamin C. Pierce: the canonical type system text -- [_Advanced Topics in Types and Programming Languages_](https://www.cis.upenn.edu/~bcpierce/attapl/) by Benjamin C. Pierce - - -## algebraic data types - -## inductive types -- https://en.wikipedia.org/wiki/Inductive_type - -## refinement types - -- [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/) -- [Refinement Types in Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-tutorial/) -- [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763) - -## dependent types - -usage -- [Programming Language Foundations](https://jscoq.github.io/ext/sf/plf/full/toc.html) -- [Programming Language Foundations in Agda](https://plfa.github.io/) - -languages -- [Coq](https://coq.inria.fr/) -- [Lean](https://lean-lang.org/) -- [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) -- [Isabelle](https://isabelle.in.tum.de/) - -implementation -- [Checking dependent types with normalization by evaluation](https://davidchristiansen.dk/tutorials/nbe/) -- [Barebones lambda cube in OCaml](https://gist.github.com/Hirrolot/89c60f821270059a09c14b940b454fd6) -- [Dependent types in 80 lines of code](https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196) - -papers -- [Turnstile+: dependent type systems as macros](https://www.williamjbowman.com/resources/wjb2019-depmacros.pdf) - -## homotopy type theory - -- [*Homotopy Type Theory*](https://homotopytypetheory.org) diff --git a/ctf/crypto.md b/ctf/crypto.md index 665ace4..7ff4bd2 100644 --- a/ctf/crypto.md +++ b/ctf/crypto.md @@ -1,14 +1,13 @@ --- layout: ctf -title: ctf/cryptography +title: some notes on cryptography --- -# cryptography for computer security +# cryptography - [cryptohack](https://cryptohack.com) - [cryptopals](https://cryptopals.org) - ## notes on cryptohack ## notes on cryptopals diff --git a/ctf/pwn.md b/ctf/pwn.md index d269699..053ea28 100644 --- a/ctf/pwn.md +++ b/ctf/pwn.md @@ -1,6 +1,6 @@ --- layout: ctf -title: ctf/binary exploitation +title: some notes on binary exploitation --- # binary exploitation diff --git a/ctf/rev.md b/ctf/rev.md index 78c95cf..ba82c48 100644 --- a/ctf/rev.md +++ b/ctf/rev.md @@ -1,6 +1,6 @@ --- layout: ctf -title: ctf/reverse engineering +title: some notes on reverse engineering --- # reverse engineering diff --git a/ctf/web.md b/ctf/web.md index d5bf6cc..93612ae 100644 --- a/ctf/web.md +++ b/ctf/web.md @@ -1,6 +1,6 @@ --- layout: ctf -title: ctf/web security +title: some notes on web security --- # web security diff --git a/plt/compilers.md b/plt/compilers.md new file mode 100644 index 0000000..d668308 --- /dev/null +++ b/plt/compilers.md @@ -0,0 +1,15 @@ +--- +layout: plt +title: computation/compilers +--- + +# compilers + +articles +- [Compiler optimizations are hard because they forget](https://faultlore.com/blah/oops-that-was-important/) +- [A tutorial on how to write a compiler using LLVM](https://tomassetti.me/a-tutorial-on-how-to-write-a-compiler-using-llvm/) + +books and courses +- [Programming Languages, Application and Interpretation](https://www.plai.org/) +- [Introduction to Compiler Construction](https://www.students.cs.ubc.ca/~cs-411/2022w2/book_top.html) +- [Design Your Own Language (book list)](https://slebok.github.io/dyol/books/index.html) diff --git a/plt/continuations.md b/plt/continuations.md new file mode 100644 index 0000000..b1566d0 --- /dev/null +++ b/plt/continuations.md @@ -0,0 +1,19 @@ +--- +layout: plt +title: computation/continuations +--- + +# continuations + +- [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) +- [By example: continuation-passing style](https://matt.might.net/articles/by-example-continuation-passing-style/) +- [How to compile with continuations](https://matt.might.net/articles/cps-conversion/) +- [**Oleg Kiselyov's writings**](https://okmij.org/ftp/continuations/) +- [An argument against call/cc](https://okmij.org/ftp/continuations/against-callcc.html) + +## continuations + +## continuation-passing style + +## deliminated continuations diff --git a/plt/effects.md b/plt/effects.md new file mode 100644 index 0000000..03b7c8e --- /dev/null +++ b/plt/effects.md @@ -0,0 +1,27 @@ +--- +layout: plt +title: computation/effects +--- + +# effects + +posts +- [Oleg Kiselyov's writings](https://www.okmij.org/ftp/) +- [Exotic Programming Ideas: Effect Systems](https://www.stephendiehl.com/posts/exotic03.html) +- [Faking algebraic effects and handlers with traits](https://blog.shtsoft.eu/2022/12/22/effect-trait-dp.html) +- [From deliminated continuations to algebraic effects](https://blog.poisson.chat/posts/2023-01-02-del-cont-examples.html) +- [OCaml effects tutorial](https://github.com/ocaml-multicore/ocaml-effects-tutorial) +- [Simple functional effects with tag unions](https://www.youtube.com/watch?v=7SidSvJcPd0) +- [Effect bibliography](https://github.com/yallop/effects-bibliography) + +papers +- [What is algebraic about algebraic effects and handlers?](https://arxiv.org/abs/1807.05923) +- [Asynchronous effects](https://dl.acm.org/doi/10.1145/3434305) + +languages +- [Koka](https://koka-lang.github.io/koka/doc/book.html) +- [Effekt](https://effekt-lang.org/) +- [Eff](https://www.eff-lang.org/) +- [Unison](https://www.unison-lang.org/) +- [Effect handlers for WebAssembly](https://wasmfx.dev/) +- [Coeffects: Context-aware programming languages](https://tomasp.net/coeffects/) diff --git a/plt/lambda-calculus.md b/plt/lambda-calculus.md new file mode 100644 index 0000000..b666ef6 --- /dev/null +++ b/plt/lambda-calculus.md @@ -0,0 +1,6 @@ +--- +layout: plt +title: computation/lambda calculus +--- + +# the lambda calculus diff --git a/plt/memory-management.md b/plt/memory-management.md new file mode 100644 index 0000000..81538be --- /dev/null +++ b/plt/memory-management.md @@ -0,0 +1,21 @@ +--- +layout: plt +title: computation/memory management +--- + +# memory management + +lobster +- [Memory Management in Lobster](https://aardappel.github.io/lobster/memory_management.html) + +nim +- [ARC/ORC in Nim](https://nim-lang.org/blog/2020/10/15/introduction-to-arc-orc-in-nim.html) +- [ORC in Nim](https://nim-lang.org/blog/2020/12/08/introducing-orc.html) +- [Destructors and Move Semantics in Nim](https://nim-lang.org/docs/destructors.html) +- [Nim's ARC/ORC and Rust's move semantics](https://paste.sr.ht/blob/731278535144f00fb0ecfc41d6ee48513233baa4) + +## reference counting + +## tracing + +## ownership diff --git a/plt/modules.md b/plt/modules.md new file mode 100644 index 0000000..1323743 --- /dev/null +++ b/plt/modules.md @@ -0,0 +1,25 @@ +--- +layout: plt +title: computation/modules +--- + +# modules + +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/) (and [slides](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](https://annas-archive.org/md5/7175434efd5620b4b117aa45a01777fa) + +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)? diff --git a/plt/monads.md b/plt/monads.md new file mode 100644 index 0000000..c59ecaa --- /dev/null +++ b/plt/monads.md @@ -0,0 +1,8 @@ +--- +layout: plt +title: computation/monads +--- + +# monads + +- [Monads in 300 words](https://lambda.xyz/blog/monads/) diff --git a/plt/paradigms.md b/plt/paradigms.md new file mode 100644 index 0000000..55c32d4 --- /dev/null +++ b/plt/paradigms.md @@ -0,0 +1,14 @@ +--- +layout: plt +title: computation/programming paradigms +--- + +# reflections on programming paradigms + +## imperative programming + +## object-oriented programming + +## functional programming + +... diff --git a/plt/patterns.md b/plt/patterns.md new file mode 100644 index 0000000..fbdc95e --- /dev/null +++ b/plt/patterns.md @@ -0,0 +1,6 @@ +--- +layout: plt +title: computation/design patterns +--- + +# ways of going about doing things diff --git a/plt/pragmatics.md b/plt/pragmatics.md new file mode 100644 index 0000000..54c413f --- /dev/null +++ b/plt/pragmatics.md @@ -0,0 +1,12 @@ +--- +layout: plt +title: computation/pragmatics +--- + +## operational semantics + +big-step vs. little-step + +## Resources: +- https://cs.stackexchange.com/questions/43294/difference-between-small-and-big-step-operational-semantics +- https://langdev.stackexchange.com/questions/3352/how-do-i-formally-define-a-programming-languages-meaning-step-by-step diff --git a/plt/semantics.md b/plt/semantics.md new file mode 100644 index 0000000..191b61c --- /dev/null +++ b/plt/semantics.md @@ -0,0 +1,8 @@ +--- +layout: plt +title: computation/semantics +--- + +# formal semantics + +## denotational semantics diff --git a/plt/syntax.md b/plt/syntax.md new file mode 100644 index 0000000..0a046a7 --- /dev/null +++ b/plt/syntax.md @@ -0,0 +1,29 @@ +--- +layout: plt +title: computation/syntax +--- + +# syntax + +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 +- [_Compilers: Principles, Techniques, Tools_](https://annas-archive.org/md5/90db32d070cfb70ca617e655d5c35529) + +## notation + +ebnf + +npegs + +## lexing + +## parsing + +cover: +- please please please lex +- handrolled parsers +- pegs and their limitations +- other varieties of parser generators (ANTLR, lalrpop, yacc...) diff --git a/plt/types.md b/plt/types.md new file mode 100644 index 0000000..d0e1729 --- /dev/null +++ b/plt/types.md @@ -0,0 +1,50 @@ +--- +layout: plt +title: computation/types +--- + +# types! ah, wonderous types! + +posts +- ✨ [**How should I read type system notation?**](https://langdev.stackexchange.com/questions/2692/how-should-i-read-type-system-notation/) +- [Programming Language Theory resources](https://steshaw.org/plt/) + +books +- ✨ [_**Types and Programming Languages**_](https://www.cis.upenn.edu/~bcpierce/tapl/) by Benjamin C. Pierce: the canonical type system text +- [_Advanced Topics in Types and Programming Languages_](https://www.cis.upenn.edu/~bcpierce/attapl/) by Benjamin C. Pierce + + +## algebraic data types + +## inductive types +- https://en.wikipedia.org/wiki/Inductive_type + +## refinement types + +- [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/) +- [Refinement Types in Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell-tutorial/) +- [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763) + +## dependent types + +usage +- [Programming Language Foundations](https://jscoq.github.io/ext/sf/plf/full/toc.html) +- [Programming Language Foundations in Agda](https://plfa.github.io/) + +languages +- [Coq](https://coq.inria.fr/) +- [Lean](https://lean-lang.org/) +- [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) +- [Isabelle](https://isabelle.in.tum.de/) + +implementation +- [Checking dependent types with normalization by evaluation](https://davidchristiansen.dk/tutorials/nbe/) +- [Barebones lambda cube in OCaml](https://gist.github.com/Hirrolot/89c60f821270059a09c14b940b454fd6) +- [Dependent types in 80 lines of code](https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196) + +papers +- [Turnstile+: dependent type systems as macros](https://www.williamjbowman.com/resources/wjb2019-depmacros.pdf) + +## homotopy type theory + +- [*Homotopy Type Theory*](https://homotopytypetheory.org) diff --git a/web/css.md b/web/css.md new file mode 100644 index 0000000..14367bc --- /dev/null +++ b/web/css.md @@ -0,0 +1,234 @@ +--- +layout: web +title: A Brief Reference for Modern CSS +--- + +# A Brief Reference for Modern CSS + +I like CSS. I really, really like CSS. I greatly enjoy just... fucking about with it, producing [pretty websites](https://apropos.codes) (egotistical, i know!) and [ugly websites](https://cursedc.tf/2023) and [weird-ass websites](https://cursedc.tf). + +But I don't like *everything* about CSS, and one of those things I don't like is how much I have to rely on references. Property names are remarkably unintuitive. And CSS is complicated! There's a lot to keep in your head, and it's ever changing - ever improving, I would say, but ever changing nonetheless. So I figured writing my *own* reference might help. + +So here is some sort of reference. If you're me, hi! I hope this was helpful. If you're not me, hi! I hope this is helpful. But you shouldn't be here really, go to the [MDN reference](https://developer.mozilla.org/en-US/docs/Web/CSS) or the [Interneting is Hard tutorial](https://www.internetingishard.com/) or something. I wrote these notes for me: they do not cover things I do not care about: very notably browser support. *Especially* vendor prefixes but also just generally: if it works in modern Chrome and modern Firefox, it's good enough for me. + +https://css-tricks.com/whats-new-since-css3/ + +## Layout + +### flow + +### absolute + +### flexbox + +### grid + +## Media Queries + +## Selectors + +**attributes** go on elements... + +**identifiers** can be selected with `#`. + +**classes** can be selected with `.`. + +### combinators + +### nested queries + +Queries can be nested!!!!!1!! + +### pseudo-classes + +### pseudo-elements + +## Elements + +Many elements have default styles provided by the browser. These are accessible at ... in Firefox, and ... in Chrome. +resource://gre-resources/html.css + +### body and friends + +```css +body { + display: block; + margin: 8px; +} +``` + +```css +html, main, header, footer, div, +section, nav, article, aside, blockquote { + display: block; +} +``` + +### formatting + +```css +b, strong { + font-weight: bolder; +} +``` + +```css +i, em { + font-style: italic; +} +``` + +```css +u { + text-decoration: underline; +} +``` + +```css +s { + text-decoration: line-through; +} +``` + +```css +q:before { + content: open-quote; +} + +q:after { + content: close-quote; +} +``` + +```css +small { + font-size: smaller; +} +``` + +```css +sub { + vertical-align: sub; + font-size: smaller; +} +``` + +```css +sup { + vertical-align: super; + font-size: smaller; +} +``` + +```css +code { + font-family: -moz-fixed; +} +``` + +### paragraphs + +```css +p { + display: block; + margin-block: 1em; +} +``` + +```css +pre { + display: block; + font-family: -moz-fixed; + white-space: pre; + margin-block: 1em; +} +``` + +### headers + +```css +h1, h2, h3, h4, h5, h6 { + display: block; + font-weight: bold; +} + +h1 { + font-size: 2em; + margin-block: .67em; +} + +h2 { + font-size: 1.5em; + margin-block: .83em; +} + +h3 { + font-size: 1.17em; + margin-block: 1em; +} + +h4 { + font-size: 1.00em; + margin-block: 1.33em; +} + +h5 { + font-size: 0.83em; + margin-block: 1.67em; +} + +h6 { + font-size: 0.67em; + margin-block: 2.33em; +} +``` + +`h1`s nested within an `article`, `aside`, `nav`, or `section` behave somewhat strangely, acting as a smaller header depending on the level of nesting. + +### lists + +```css +li { + display: list-item; + text-align: match-parent; +} +``` + +```css +ul, menu { + display: block; + counter-reset: list-item; + margin-block: 1em; + padding-inline-start: 40px; + list-style-type: disc; +} +``` + +```css +ol { + display: block; + counter-reset: list-item; + margin-block: 1em; + padding-inline-start: 40px; + list-style-type: decimal; +} +``` + +Nested lists have no top or bottom margins. The `list-style-type` of unordered lists changes with depth: from a `disc`, to a `circle`, to a `square`. + +### meta + +```css +head, link, meta, title, style, script { + display: none; +} +``` + +___ are invisible. + +## Properties + +There are a *lot* of properties, of various elements, and things. + +`property left right center up` or whatever +this seems consistent and i don't know it diff --git a/web/html.md b/web/html.md new file mode 100644 index 0000000..6dcdef6 --- /dev/null +++ b/web/html.md @@ -0,0 +1,217 @@ +--- +layout: web +title: A Quick Guide to Modern HTML +--- + +# A Quick Guide to Modern HTML + +This guide is a work in progress! + +Modern HTML is a remarkably simple and coherent standard. + +## Basic HTML + +HTML is a *markup language* used for content on the web. It is composed of *tags*, that may be *nested* within each other to form a *document tree*. It is *semantic*: every tag + +and many tags indeed hold no purpose other than indicating ... + + +Every website you visit is composed of HTML, which alongside with styling via CSS... Modern websites are composed of somewhat atrocious amounts of + +Web browsers receive HTML documents from a web server or from local storage and render the documents into multimedia web pages. HTML describes the structure of a web page semantically and originally included cues for its appearance. + +HTML elements are the building blocks of HTML pages. With HTML constructs, images and other objects such as interactive forms may be embedded into the rendered page. HTML provides a means to create structured documents by denoting structural semantics for text such as headings, paragraphs, lists, links, quotes, and other items. HTML elements are delineated by tags, written using angle brackets. Tags such as and directly introduce content into the page. Other tags such as

and

surround and provide information about document text and may include sub-element tags. Browsers do not display the HTML tags but use them to interpret the content of the page. + + +HTML is composed of *tags*. These tags are enclosed in angle brackets + +There are quite a few tags, but not overwhelmingly many. Here they all are. + +if your tag is not reserved, you can kinda just write whatever?? i like doing this + +There are about XX important tags. Here they all are. + +## Style + +- [` `](https://developer.mozilla.org/HTML/Element/b) or [` `](https://developer.mozilla.org/HTML/Element/strong): bold text +- [` `](https://developer.mozilla.org/HTML/Element/i) or [` `](https://developer.mozilla.org/HTML/Element/em): italic text +- [` `](https://developer.mozilla.org/HTML/Element/s): ~~struckthrough~~ text +- [` `](https://developer.mozilla.org/HTML/Element/u): underlined text +- [` `](https://developer.mozilla.org/HTML/Element/q): quoted text +- [` `](https://developer.mozilla.org/HTML/Element/small): small text +- [``](https://developer.mozilla.org/HTML/Element/sub): _subtext +- [``](https://developer.mozilla.org/HTML/Element/sup): ^supertext +- [` `](https://developer.mozilla.org/HTML/Element/code): text styled like code + +Some emphasis must be put: these tags are **semantic**. They are not for styling! You have a much more expressive form of styling with CSS! +Given the existence of a quote key on most ASCII keyboards, this is not very useful, unless you're a stickler for Unicode quotes. + +## Wrappers + +These wrappers have no style associated with them, but are *semantically meaningful*. or is that true? they are all `block`, no? + +`` +`` +`

` + +```css +

+``` + +`

` +`

` +`
` +`

` +` ` (or below) + +## Content + +```css + +``` +`` +`