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

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

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

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

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

We're going live with Software Foundations Speedrun. Today we finish Logic.v www.twitch.tv/typeth...

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

Embarrassing situation on MathOverflow where, in answer to the same question, we have a proof that alternative division algebras in characteristic 2 are associative, and a counterexample showing that they aren't. So, who's wrong? mathoverflow.net/q/485668/17064

We're about to go live to continue working on Functional Programming in Lean 4. Today we will be looking at how to start a Project from scratch and hopefully we'll finish chapter 2. www.twitch.tv/typeth...

Hey, have you seen the exclusive Type Theory merch? store.typetheoryfora... Enjoy our 10% off sales! Use the discount code `typetheory`

2️⃣ "Will Computers Prove Theorems?" with Kevin Buzzard A provocative journey to mathematics' future where AI might find patterns humans have missed for centuries. Kevin makes a compelling case for why mathematicians must engage now. Watch: podcasts.ox.ac.uk/will-compute...

1️⃣ "Formalizing the Future" with Leo de Moura A visionary look at how Lean shatters the trust bottleneck in human knowledge, and reveals how machine-checkable proof is transforming mathematics, software verification and AI in ways impossible just years ago. Watch: podcasts.ox.ac.uk/formalizing-...

We're going live now to continue our Software Foundations Speedrun. Join us to learn more about Rocq! www.twitch.tv/typeth...

We're about to go live on twitch to continue our Functional Programming in Lean4 series. www.twitch.tv/typeth...

if Haskell code "has no side-effects" then how could my girlfriend leave me claiming that I "never shut up about haskell code"?