In case you missed it, watch this clip from our interview with Andrej Bauer. I love when CS researchers can articulate a philosophy behind their work, and Andrej DELIVERS www.youtube.com/watch?v=GcTF...

🎉 5 YEARS OF TYPE THEORY FORALL 🎉 To celebrate, I sat down with Andrej Bauer. Student of Dana Scott. A mind equally at home in math and CS. One of the clearest thinkers in Type Theory. We dive into Constructivism, Dialectica, Effect Handlers, and AI. This one is special.

🎙️ 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

Going 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.

@krismicinski's build a compiler in Five Projects

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.

Going 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...

Feeling 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

Pedro 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

true friendship 🥹

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

Interested in Rocq, Haskell, or OCaml? Or looking for guidance on grad school applications in Computer Science (PL + Formal Methods)? Here’s how we can help: 1/5

We still need to sell one or two shirts to cover the merch store operational costs, send help 🫠 store.typetheoryfora...

This is your weekly reminder that we have a store with awesome Type Theory / PLT merch. Check it out at store.typetheoryfora...

This is your weekly reminder that we have a store with awesome Type Theory / PLT merch. Check it out at store.typetheoryfora...

This is your weekly reminder that we have a store with awesome Type Theory / PLT merch. Check it out at store.typetheoryfora...

Check out the latest captivating interview featuring ACM Fellow Derek Dreyer! He opens up about battling impostor syndrome and failure in grad school, his aspirations to be a movie director, and his groundbreaking research on Rust

Hey guys, we've got some pretty cool new mugs at the ttfa store ttforall.myshopify.com/

Check out this hilarious stand-up routine where Philip Wadler explains computability - it's pure gold!

"In most universities nowadays—and this seems to be true almost everywhere—academic staff find themselves spending less and less time studying, teaching, and writing about things, and more and more time measuring, assessing, discussing, and quantifying the way in which ...

"SQL, Lisp, and Haskell are the only programming languages that I've seen where one spends more time thinking than typing." — Philip Greenspun

"How to Present a Paper" by Leslie Lamport, 1979 lamport.azurewebsite...

Why Lean 4 replaced OCaml as my Primary Language kirancodes.me/posts/...

This is your weekly reminder that we have a store with awesome Type Theory / PLT merch. Check it out at store.typetheoryfora...

Super exciting update! 🚀 Join our new 1o1 mentorship program to level up in functional programming: Rocq, Haskell, and OCaml. Get expert guidance on Grad School Applications worldwide. Reach out at [email protected] to get started!

Big news! We are launching a new sponsorship program for orgs passionate about Programming Languages & Type Theory. Reach a highly engaged, technical audience! Email [email protected] for details. Please RT to help us reach big companies and deepen our content focus!

Type structure is a syntactic discipline for enforcing levels of abstraction. – Reynolds [1983]

This is your weekly reminder that we have a store with awesome Type Theory / PLT merch. Check it out at store.typetheoryfora...

Liquid Haskell Quick Start ninioartillero.githu...

Our discord community is starting a new Software Foundations Study group to learn PLT and the Rocq Theorem Prover, if you're interested feel free to join discord.com/invite/D...

Brazil's cutting-edge security includes deploying SMT solvers right on the streets!

Dive into our latest episode from Zurihac with Lennart. It's hot off the press! Watch it here: www.typetheoryforall...

Participating in @zurihac in June was an absolute blast! We got up to some seriously cool stuff, including interviewing folks about their love (and hate) for Haskell. Check out the interviews here: www.youtube.com/watc...

We're going live in a few minutes to continue working on our Nes Emulator in Rust Today we push our PPU to render our first game! Join us at www.twitch.tv/typeth...

So apparently they sell Calculus of Inductive Constructions at France