diff options
Diffstat (limited to 'computation')
| -rw-r--r-- | computation/compilers.md | 14 | ||||
| -rw-r--r-- | computation/effects.md | 1 | ||||
| -rw-r--r-- | computation/syntax.md | 18 | ||||
| -rw-r--r-- | computation/types.md | 38 |
4 files changed, 54 insertions, 17 deletions
diff --git a/computation/compilers.md b/computation/compilers.md index b3b1769..b9db36d 100644 --- a/computation/compilers.md +++ b/computation/compilers.md @@ -1,8 +1,10 @@ -# Compilers +# 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 +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/effects.md b/computation/effects.md index ac11fae..98312c5 100644 --- a/computation/effects.md +++ b/computation/effects.md @@ -7,6 +7,7 @@ posts - [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) diff --git a/computation/syntax.md b/computation/syntax.md index 7dd776d..29e8c48 100644 --- a/computation/syntax.md +++ b/computation/syntax.md @@ -1,19 +1,19 @@ -# Syntax +# syntax -## Resources - -Articles +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) +books +- [_Compilers: Principles, Techniques, Tools_](https://annas-archive.org/md5/90db32d070cfb70ca617e655d5c35529) + +## notation -## Notation +ebnf -## Lexing +## lexing -## Parsing +## parsing cover: - please please please lex diff --git a/computation/types.md b/computation/types.md index 2edfe7c..2124175 100644 --- a/computation/types.md +++ b/computation/types.md @@ -1,11 +1,45 @@ # types! ah, wonderous types! -## Resources +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 -- *Types and Programming Languages* 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) |