---
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)