---
# System prepended metadata

title: Resources

---

##### Haskell 101

- [Learn You a Haskell for Great Good: A Beginner's Guide (Miran Lipovača)](https://learnyouahaskell.com/)
- [Haskell - Wikibook](https://en.wikibooks.org/wiki/Haskell)

##### (Not Quick) Start

- [Modern dependent type theory (Lecture note spring 2024)](https://www.danielgratzer.com/courses/type-theory-s-2024/index.html)
- [Agda Tutorial (people.inf.elte.hu/divip)](https://people.inf.elte.hu/divip/AgdaTutorial/Index.html)
- [Introduction to Type Theory (herman@cs.ru.nl, 2008)](https://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf)
- [type theory (ncatlab.org)](https://ncatlab.org/nlab/show/type+theory)
- [Introduction to Univalent Foundations of Mathematics with Agda (m.escardo@bham.ac.uk)](https://arxiv.org/abs/1911.00580)

##### Overviews

- [relation between type theory and category theory (ncatlab.org)](https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory) 
- [Group-like structures (en.wikipedia.org)](https://en.wikipedia.org/wiki/Template:Group-like_structures)
- [Major topics in Foundations of Mathematics (en.wikipedia.org)](https://en.wikipedia.org/wiki/Template:Foundations-footer)

##### Type Theory

- [Homotopy Type Theory: Univalent Foundations of Mathematics (Univalent Foundations Program of IAS,  2013)](https://arxiv.org/abs/1308.0729)
- [The Lambda Calculus (plato.stanford.edu)](https://plato.stanford.edu/entries/lambda-calculus/)
- [Function Totality: Abstraction Tool in Programming (dimjasevic.net)](https://dimjasevic.net/marko/2018/11/20/function-totality-abstraction-tool-in-programming/)

##### *Uncategorized*

- [Structure and Interpretation of Computer Programs (mit.edu, 1996)](https://mitp-content-server.mit.edu/books/content/sectbyfn/books_pres_0/6515/sicp.zip/index.html)
- [Linear Logic (plato.stanford.edu)](https://plato.stanford.edu/entries/logic-linear/)
- [Object-oriented programming in dependent type theory(a.g.setzer@swan.ac.uk, 2006)](https://www.cs.nott.ac.uk/~psznhn/TFP2006/Papers/26-AntonSetzer-OOPInDependentTypeTheory.pdf)
- [What is Agda? — Agda 2.6.4.1 documentation](https://agda.readthedocs.io/en/v2.6.4.1/getting-started/what-is-agda.html)
- [Introductory books on Category Theory (Youtube video in Japanese)](https://youtu.be/AFZ-KC8zcEk)
    - [Basic Category Theory (Tom Leinster, 2016)](https://arxiv.org/abs/1612.09375)
    - Category Theory (Steve Awodey, 2010)
    - Categories for the Working Mathematician (Saunders MacLane, 1971)
    - [Category Theory in Context (Emily Riehl, 2014)](https://math.jhu.edu/~eriehl/context.pdf)

##### Links

- [Functional Thursday: FP Community in Taipei (youtube.com)](https://www.youtube.com/@thursdayfunctional9801)
- [FLOLAC (Formosan Summer School on Logic, Language, and Computation)](https://flolac.iis.sinica.edu.tw)
- [Kerodon: an online resource for homotopy-coherent mathematics (lurie@isa)](https://kerodon.net/)
- [nlab (ncatlab.org)](https://ncatlab.org/nlab/show/HomePage)

##### Authors' pages (Maybe useful)

- [Jacob Luries \<lurie@isa>](https://www.math.ias.edu/~lurie/)
- [Herman Geuvers \<herman@cs.ru.nl>](http://cs.ru.nl/~herman/)

*This is a reading list created by a functional programming study circle that is also new to type theory.* 