diff options
| author | JJ | 2023-11-24 03:35:03 +0000 |
|---|---|---|
| committer | JJ | 2023-11-24 03:35:03 +0000 |
| commit | 384af43d4220eb93abe06668210c594923fb9a8c (patch) | |
| tree | 3762c806c6034bb1d52d2ecef76bb43f79509298 /computation/types.md | |
| parent | 426d431d03599b65dee1ddffd8923098cbaa79b0 (diff) | |
meow
Diffstat (limited to 'computation/types.md')
| -rw-r--r-- | computation/types.md | 38 |
1 files changed, 36 insertions, 2 deletions
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) |