Type Theory Forall

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 contact@typetheoryforall.com to get started!

4/ By partnering with us, you're investing in content that continues to educate and influence over time, connecting your brand with a dedicated and growing community interested in the foundations of computing.

Join us in shaping the future of PL contact@typetheoryforall.com

3/ Our sponsorship offers superior value compared to traditional PL conferences. While conference tables can cost up to $20K+ for just a week of exposure, our podcast episodes live virtually forever, reaching a far greater, global audience than any single conference.

2/ Our commitment to high-quality content is unwavering. We've hosted esteemed figures like Leo de Moura, Kevin Buzzard, Lawrence Paulson, and Conal Elliott, bringing unparalleled insights to our audience. We even have live episodes, like our session at Zurihac!

1/ We've been building credibility for over 4.5 years, delivering more than 80 hours of in-depth content. We're not a fleeting trend; we're a consistent and reliable platform in the PL community.

Big news! We are launching a new sponsorship program for orgs passionate about Programming Languages & Type Theory.

Reach a highly engaged, technical audience! Email contact@typetheoryforall.com 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...

Get inspired by the largest Haskell gathering in the world – straight from Zurich! What makes Haskell so special? And what drives people crazy about it? In this video, developers, researchers, and Haskell enthusiasts from all over the world answer two simple questions: 👉 What do you love about Hask Impressions of ZuriHac, and Why We Love (and Hate) Haskell | Voices from ZuriHac 2025

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

TypeTheoryForall - Twitch Coding a Nes Emulator in Rust

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

"... and in neither case does your code stand much chance of being efficient. In order to ensure that your program is efficient, you need to know what it is doing, and if your code is ugly, you will find it hard to analyze." - Richard O’Keefe, The Craft of Prolog

"Elegance is not optional. There is no tension between writing a beautiful program and writing an efficient program. If your code is ugly, the chances are that you either don’t understand your problem or you don’t understand your programming language" ...

I'm pleased to announce OxCaml!

OxCaml is Jane Street's branch of OCaml. We've given it a new name and a snazzy logo, and done a bunch of work to make it easy for people to try.

Attending @zurihac was a total blast! Stay tuned for exciting updates coming your way soon!

Check out the latest episode where I chat with Nicolas Tabareau from Inria's Rocq team about the Coq → Rocq rebranding, LLMs, sort polymorphism, MetaRocq, and the future of proof assistants. Watch the episode here: www.typetheoryforall...

Type Theory Forall - YouTube Share your videos with friends, family, and the world

A massive thank you to all our backers for making our Zurihac crowdfunding a success! Unbelievably, we hit $2000 in under a month of streaming! Exciting Haskell content is on the horizon next week! 🚀

In the meantime, catch our newest YouTube shorts here: www.youtube.com/@typ...

By the way we are only $20 off from our crowdfunding to take us to Zurihac! It would be awesome if you guys could assist us! :))

ko-fi.com/typetheory...

TypeTheoryForall - Twitch Functional Programming in Lean4!

We are about to go live and continue working the Software Foundations Speedrun using Rocq. Today we should finish IndProp.v (Inductively Defined Propositions)

www.twitch.tv/typeth...

Twitch Twitch is the world's leading video platform and community for gamers.

We're about to go live with our Functional Programming in Lean4 Series! Today we'll work on Chapters 3 and 4, Proofs and Type Classes!

www.twitch.tv/typeth...

In a world focused on practicality, Donald Knuth's perspective on Computer Science being an Art is a breath of fresh air. We should all dive into his philosophical insights in the Turing Lecture "Computer Programming as an Art" here: dl.acm.org/doi/10.11...

🚨 New drop alert! 🚨
Support Type Theory Forall and rep your love for types with our official merch 🧵✨

🛒 Check out the store: store.typetheoryfora...
🎁 Use code typetheory for 10% off — limited time only!

Let the world know you quantify forall the right reasons. 🔥

TypeTheoryForall - Twitch Software Foundations Speedrun!

We're going live with Software Foundations Speedrun. Today we finish Logic.v

www.twitch.tv/typeth...