diff options
| author | JJ | 2024-01-05 02:37:28 +0000 |
|---|---|---|
| committer | JJ | 2024-01-05 02:37:28 +0000 |
| commit | 439c5d3ef5fb8b8ebba28d45088d9b91db7418ac (patch) | |
| tree | 279051b346a86c782b3b7ad3a954f1f8dab9bb54 /computation/types.md | |
| parent | 5ffac59a93388e16e90dbdd1c4f68d6a2f2c057a (diff) | |
meow
Diffstat (limited to 'computation/types.md')
| -rw-r--r-- | computation/types.md | 50 |
1 files changed, 0 insertions, 50 deletions
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) |