| 📌 |
📚 [MEGATHREAD] Type Theory Resources — Books, Lectures, Papers
Sticky
Announce
|
218
41,200 views
|
admin-nyanko
⭐ Admin · 4,201 posts
|
ProofKitten
Today, 08:14
[→ last post]
|
| 📌 |
🐾 Ask a Dumb Question Thread (no judgment!)
Sticky
|
876
88,500 views
|
admin-nyanko
⭐ Admin · 4,201 posts
|
MewMewMonad
Today, 11:47
[→ last post]
|
| 🔥 |
Dependent Types Are Not the Answer to Everything (fight me)
🔥 Hot
Poll
|
412
19,840 views
|
PracticalPurr
🐱 Regular · 891 posts
|
TypeNihilistKat
Today, 13:02
[→ last post]
|
| 💬 |
Lean 4 vs Rocq in 2025 — which do you actually use?
Hot
Poll
|
187
9,340 views
|
FormalFelinae
🐈 Veteran · 2,103 posts
|
RocqCatFan
Today, 09:55
[→ last post]
|
| 💬 |
HoTT: Any Practical Applications Yet or Are We Just Doing Math for Fun
Hot
|
143
7,612 views
|
UnivalentUnicorn
🐾 Regular · 554 posts
|
PathsAllTheWayDown
Yesterday, 22:18
[→ last post]
|
| 💬 |
Session Types Megathread — Resources, Papers, Discussion
New
|
98
4,207 views
|
LinearPaws
🐱 Regular · 701 posts
|
PiTypesPurr
Today, 10:33
[→ last post]
|
| 💬 |
The Curry-Howard Correspondence Appreciation Thread 🫶
Poll
|
79
6,040 views
|
ProofsArePrograms
🐾 Regular · 1,240 posts
|
LambdaCatgirl
Yesterday, 14:50
[→ last post]
|
| 💬 |
GADTs: Dependent Types at Home (Haskell/OCaml edition)
New
|
67
3,891 views
|
GhostlyGADT
🐱 Regular · 334 posts
|
PatternMatchPurrr
Today, 07:41
[→ last post]
|
| 💬 |
Refinement Types vs Full Dependent Types — when is each appropriate?
|
52
3,210 views
|
RefinementRawr
🐾 Regular · 477 posts
|
LiquidTypeKitty
2 days ago
[→ last post]
|
| 💬 |
Parametricity and Free Theorems — getting theorems for free since 1989
New
|
41
2,104 views
|
WadlerCatFan
🐱 Member · 212 posts
|
PolyPurrfect
Today, 06:22
[→ last post]
|
| 💬 |
Totality Checking is Actually Based and You Should Use It
|
38
1,987 views
|
TotallyTyped
🐾 Regular · 589 posts
|
PartialPawsGirl
3 days ago
[→ last post]
|
| 💬 |
Type Inference: Hindley-Milner vs Bidirectional — a comparison
New
|
33
1,750 views
|
InferenceEngine9
🐱 Member · 145 posts
|
BidirBrigade
Today, 12:19
[→ last post]
|
| 💬 |
Cubical Type Theory ELI5 — I keep hearing about it but am scared
|
29
2,841 views
|
CubeScared
🐾 Newcat · 44 posts
|
CubicalCatgirl
4 days ago
[→ last post]
|
| 💬 |
Universe Polymorphism in Rocq — impredicativity crimes and how to avoid them
|
27
1,330 views
|
ProposNyan
🐱 Regular · 398 posts
|
CoCKitty
5 days ago
[→ last post]
|
| 💬 |
Effect Systems and Algebraic Effects — where do they fit in the type theory zoo?
New
|
24
1,102 views
|
EffectfulNekomata
🐱 Member · 187 posts
|
FreeMonadFurr
Today, 01:44
[→ last post]
|
| 💬 |
Agda vs Idris 2 — is the difference meaningful for everyday use?
|
21
1,480 views
|
AgdaAdorer
🐾 Regular · 622 posts
|
IdrisPurrsuit
1 week ago
[→ last post]
|
| 💬 |
Normalization by Evaluation — please explain like I have paws
|
44
2,680 views
|
NbENewbie
🐱 Newcat · 23 posts
|
SemanticsSiamese
6 days ago
[→ last post]
|
| 💬 |
Setoid Hell — commiserating and coping strategies
Poll
|
57
3,508 views
|
QuotientQueen
🐾 Regular · 755 posts
|
HITHoarder
3 days ago
[→ last post]
|
| 💬 |
The Linear Types / Rust Ownership Connection — oversimplification or legit?
|
19
1,250 views
|
BorrowChecker42
🐱 Member · 156 posts
|
AffineCat
1 week ago
[→ last post]
|
| 💬 |
Intrinsically Typed Interpreters in Agda — a walkthrough
New
|
14
892 views
|
AgdaAdorer
🐾 Regular · 622 posts
|
IntrinsicNeko
Today, 04:18
[→ last post]
|
| 💬 |
Type-Driven Development — is this actually how you use Idris or is it a meme
|
31
2,015 views
|
TDDKittyGirl
🐱 Regular · 310 posts
|
IdrisPurrsuit
5 days ago
[→ last post]
|
| 🔒 |
Intensional vs Extensional Equality — [LOCKED: became a flame war]
Locked
|
118
5,502 views
|
EqEqEq
🐾 Regular · 204 posts
|
admin-nyanko
2 weeks ago
[→ last post]
|