A community-maintained collection of textbooks, lecture series, paper reading groups, proof assistant tutorials, and navigational guides for the serious type-theoretic catgirl. Post your finds, ask for rec's, and share your reading notes. All skill levels welcome β but please tag your difficulty level appropriately.
[book], [agda], [lean], [video], [free] in your thread titles.
| Thread | Replies | Views | Last Post | |
|---|---|---|---|---|
π |
pinned
megathread
π [MEGATHREAD] The Master Type Theory Resource List β books, courses, videos, tools
by mrrphType
Β· community wiki Β· last updated 2 days ago
|
512replies | 28.4kviews |
2 days ago
cubical-paws
added PLFA Lean4 port link
|
π |
pinned
πΊοΈ Beginner's Roadmap: From "what is a type?" to dependent type theory in 6 months
by Ξ£Catgirl
Β· guide Β· 8 months ago
|
89replies | 12.1kviews |
1 week ago
Ξ»-neko
re: where does CPDT fit in...
|
| ββ regular threads ββββββββββββββββββββββββββββββββββββββββββ | ||||
π₯ |
hot
book
hott
[Book Club] HoTT Book β Homotopy Type Theory: Univalent Foundations of Mathematics | reading group week 7
by HoTTcafΓ©
Β· ongoing since 3 months ago Β· Chapter 3 this week
|
203replies | 9.3kviews |
4 hours ago
univalence-enjoyer
the path induction stuff clicked for me when...
|
π₯ |
hot
book
free
TAPL vs. PFPL β which should I read first? (Benjamin Pierce vs. Robert Harper)
by Ξ΄-type
Β· 2 weeks ago
|
78replies | 6.2kviews |
yesterday
mrrphType
PFPL lacks type inference coverage that TAPL has
|
π |
agda
free
book
[Resource] PLFA β Programming Language Foundations in Agda (Wadler, Kokke, Siek) | tips & errata
by wadler-stan
Β· 5 months ago
|
55replies | 4.8kviews |
3 days ago
coalgebraNeko
stuck on the Subtyping chapter, any hints?
|
π |
book
free
[Book] CPDT β Certified Programming with Dependent Types (Adam Chlipala) | study group
by chlipala-appreciator
Β· 1 month ago
|
41replies | 3.1kviews |
5 days ago
tactic-paws
the tactic automation chapter is purring along...
|
π¬ |
video
free
agda
[Videos] Best Agda lecture series on YouTube β Conor McBride, Philip Wadler, Peter Selinger
by cubical-paws
Β· 3 months ago
|
66replies | 5.5kviews |
6 days ago
emacs-neko
McBride's OPLSS lectures are SO good nyaa~
|
π¬ |
video
free
lean
[Lean 4] Best free tutorial resources β Theorem Proving in Lean 4, Mathlib docs, community guides
by mathlib-kitty
Β· 6 weeks ago
|
49replies | 4.1kviews |
2 days ago
lean-nyan
Functional Programming in Lean is also great for...
|
πΊοΈ |
free
How to actually navigate nLab without losing your mind β tips, tricks & entry points
by nLab-explorer
Β· 4 months ago
|
93replies | 7.7kviews |
1 week ago
topos-neko
start at "type theory" not "homotopy type theory" trust
|
π |
paper
hot
[Paper Reading Group] Bi-weekly CGPA paper club β current: "Cubical Agda: A Dependently Typed PL with Univalence and HITs"
by Ξ£Catgirl
Β· ongoing Β· 7 months old
|
134replies | 8.9kviews |
12 hours ago
cubical-paws
section 4.3 interval type semantics... halp
|
π |
video
free
hott
[Videos] HoTTEST Summer School 2022 β free online lectures by EscardΓ³, Licata & friends (Agda-based)
by HoTTcafΓ©
Β· 9 months ago
|
57replies | 5.2kviews |
3 weeks ago
univalence-enjoyer
Lecture 6 finally made HITs click for me!!
|
π |
book
[Book] ATTAPL β Advanced Topics in Types and Programming Languages (Pierce, ed.) | which chapters first?
by refinement-chan
Β· 2 months ago
|
32replies | 2.8kviews |
2 weeks ago
mrrphType
ch. 2 (effect types) and ch. 5 (subtyping) are independent
|
π |
video
free
[Course] OPLSS (Oregon PL Summer School) free lecture videos β which years/tracks are essential?
by theorem-catgirl
Β· 5 months ago
|
44replies | 3.7kviews |
4 weeks ago
propositions-as-cats
2013 and 2019 are the goat years imo
|
π |
paper
Best intro to Lambek-Scott / Curry-Howard-Lambek correspondence papers? (for catgirls who know neither CT nor TT)
by newkitten99
Β· 3 weeks ago
|
29replies | 2.1kviews |
5 days ago
topos-neko
Awodey's CT book ch. 1-4 first, then Lambek&Scott
|
π |
lean
agda
free
Agda vs. Lean 4 vs. Coq/Rocq for learning β which proof assistant to start with in 2025?
by newkitten99
Β· 1 month ago
|
87replies | 6.8kviews |
3 days ago
lean-nyan
Lean 4 has better tooling but Agda has cuter Unicode
|
π |
book
free
[Book] Software Foundations series (Pierce et al.) β vols. 1-6, all free online | progress thread
by coqNyan
Β· 7 months ago
|
71replies | 5.0kviews |
1 week ago
tactic-paws
Vol. 2 PLF is where it gets real good
|
π |
locked
book
[Locked] PFPL errata & typos thread β moved to wiki, see sidebar link
|
38replies | 2.3kviews |
2 months ago
Ξ£Catgirl
locked - see /wiki/pfpl-errata
|