blob: d0e1729e0be7c3a6171fe7b896288be795090fe6 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
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)
|
