@ttforall.bsky.social
Making Type Theory, Programming Languages and Formal methods more accessible! http://typetheoryforall.com
β’ How modern compilers enable secure computation
β’ Whether deeply learning Category Theory actually makes you a better PL researcher
β’ The realities of mental health and sustaining rhythm during a PhD
If youβre into PL, CT, or the human side of research, youβre going to love this one.
ποΈ New Type Theory Forall Episode!
#57 β Compilers for Privacy-Preserving Computation, Category Theory, and Keeping a Good Rhythm in Your PhD
This week I talk with Rhagav Malik, fresh off his PhD defense on compilers for privacy-preserving computation. We dig into:
My Spotify Wrapped
04.12.2025 18:26 β π 4 π 0 π¬ 0 π 0Going live now!
Continuing our Lean 4 Series β today we continue working on MIL, this time on Order and divisibility!
This is part of our ongoing fundraiser to replace my iPhone camera with a proper setup.
Every tip helps!
βοΈko-fi.com/typetheory...
www.twitch.tv/typeth...
Last days of our Cyber Monday 15% OFF at the ttfa store!
Mugs, hoodies, shirts β perfect gifts for your nerdiest friends this holiday season.
Enjoy it before it ends: store.typetheoryfora...
A couple weeks ago I had the great pleasure of inviting Rustan Leino (of Dafny fame) on my podcast, to talk about all sorts of logic stuff!
Part II to come soon!
open.spotify.com/episode/4d9J...
A fresh episode of Type Theory Exists is live!
Featuring my Gothenburg talk on the evolution of CS through the eyes of Type Theory β Turing, Church, CurryβHoward, and beyond.
π Only for patrons β join us to unlock it:
π¨ BLACK FRIDAY SALE! π¨
The entire Type Theory Forall shop is 15% OFF β mugs, shirts, hoodies, literally everything.
Only until the end of the month. Donβt miss it!
ππ₯ store.typetheoryfora...
Discount is automatically applied at checkout.
My five-project (along with slides, video lectures, etc.) compilers course has all projects now available online free: kmicinski.com/functional-p.... Five projects have you incrementally build a compiler for a substantial language, including functions, mutation, loops, vectors, etc.
24.11.2025 03:26 β π 25 π 11 π¬ 0 π 2Going live now! Continuing our Lean 4 Series β today I'll start working on Mathematics in Lean
This is part of our ongoing fundraiser to replace my iPhone camera with a proper setup. Every tip helps! π
βοΈko-fi.com/typetheory...
www.twitch.tv/typeth...
π¨ BLACK FRIDAY SALE! π¨
The entire Type Theory Forall shop is 15% OFF β mugs, shirts, hoodies, literally everything.
Only until the end of the month. Donβt miss it!
ππ₯ store.typetheoryfora...
Discount is automatically applied at checkout.
Going live now!
Continuing our Lean 4 Series β today Iβll be learning Tactics on stream.
This is part of our ongoing fundraiser to replace my iPhone camera with a proper setup. Every tip helps! π
βΆοΈ www.twitch.tv/typetheoryfo...
βοΈ ko-fi.com/typetheoryfo...
A new book on the history of control structures by the creator of #OCaml himself @camlist.bsky.social xavierleroy.org/control-stru...
05.11.2025 12:00 β π 15 π 5 π¬ 0 π 1Feeling the pull back to academia?
Whether youβre applying for grad school or looking to transition from industry into research, our mentorship program can guide you.
We still have open slots for this season!
β typetheoryforall.com/mentorship
types slow me down in the way that red lights slow me down when i'm driving
04.11.2025 11:57 β π 5 π 1 π¬ 2 π 0Pedro Abreu aka #TypeTheoryForall had an epic conversation with me about all things programming languages, out now on the podcast.
www.typetheoryforall.com/episodes/the...
#LiquidTypes are a lightweight way to specify and check code properties. What stands in the way of more widespread adoption?
Today at #SPLASH 2025 / @icfp-conference.bsky.social: @catarinavgamboa.bsky.social will re-present our #PLDI2025 paper on Usability Barriers for Liquid Types.
We still have a few spots open this week for 1:1 mentorship sessions on grad school applications and research careers.
If youβre applying to PhD programs or navigating advisor selection, this might be the perfect time to start.
π typetheoryforall.com/mentorship
I'm not sure how to implement the solution without typeclasses though, but I think it should be doable
08.10.2025 22:00 β π 2 π 0 π¬ 0 π 0Datatypes Γ la Carte: www.cambridge.org/core/service...
08.10.2025 21:59 β π 2 π 0 π¬ 1 π 0
A meme showing two hobbits from Lord of the Rings looking exhausted and dirt-covered, with text reading 'I can't carry your null pointers for you, but I can carry you to OCaml!' - a programming humor mashup of Sam's famous quote about carrying Frodo, replacing the Ring with null pointers and Mount Doom with the OCaml programming language.
true friendship π₯Ή
04.10.2025 15:32 β π 18 π 5 π¬ 0 π 0
How do we know that the semantics of a programming language are right?
My latest Programming Language Pragmatics video covers type soundness: the static and dynamic semantics of a language fit together, so that if a program type checks, it will not experience unexpected type errors when it runs.
there's a priest in Rome who lives on a top of a mountain so high, nobody but him is able to climb there
they call him the Inaccessible Cardinal
ur type so fat it requires large elimination
29.09.2025 08:57 β π 15 π 4 π¬ 3 π 0That's a good one. I love it! π
29.09.2025 10:31 β π 1 π 0 π¬ 0 π 0Schedule a free initial session: calendar.app.google/...
Or email us at contact@typetheoryforall.com
5/5
Weβve taught:
β’ Introduction to Logic
β’ Programming in Java, C, and Python
β’ Abstract Algebra
β’ Object-Oriented and Functional Programming
β’ Graduate and Undergraduate Programming Languages
From fundamentals to advanced PL and logic, we help students at every stage.
4/5
Our background:
β’ 10+ years in Programming Languages and Formal Methods (academia + industry)
β’ 7+ years teaching and mentoring hundreds of students
β’ ACM Best Teaching Assistant Award (Purdue University, 2018)
3/5
