Type Theory Forall

wiki.alcidesfonseca.com Fall 2026 Recommendations for AI in Higher Education by Alcides Fonseca

23 May 2025

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

Type Theory Forall reposted

Alcides Fonseca

@handle.invalid

10 Sept

How to adapt CS degrees to AI? Here's my take: wiki.alcidesfonseca.com/blog/fall-20... looking for feedback from you.

twp.aiyoutu.be#26 Mechanizing Modern Mathematics - Kevin Buzzard

10 Sept

FLT formalized in Lean by AI Navier–Stokes attacked by AI, with the result formalized in Lean Autoformalization is moving fast Three years ago I interviewed Kevin Buzzard about his vision for mechanizing modern mathematics It might be time to revisit that conversation:

5 Sept

How should we teach Programming Languages in the age of AI? New TTFA episode! 🎙️ 1/3

5 Sept

I sat down with @shriram.bsky.social to talk about PL education, how LLMs are changing the way students learn programming, and what we should actually be teaching when AI can increasingly write the code for us. 2/3

5 Sept

We also dive into Racket, programming language design, and Shriram’s decades of experience thinking about how we teach people to reason about programs. A fascinating conversation! ▶️ https://twp.ai/4hvacX 3/3

twp.aiyoutu.beyoutu.be

19 Aug

twp.aiivan-gavran.github.ioThe Case Against Formal Verification, 50 Years Later - Ivan Gavran

16 Aug

This blog post gives quite an interesting overview of where AI+FV sits atm

7 Aug

This is fantastic news. A new effort is underway to produce a Revised Haskell 2010 Language Report—updating the language specification after 16 years while keeping a well-defined, implementable standard. https://twp.ai/9OZs47

7 Aug

How do you add static types to one of the largest PHP codebases on the planet? I sat down with Julien Verlaguet, one of the creators of Hack, to hear the story behind one of the most ambitious language migration efforts ever attempted. 1/2

twp.aiyoutu.beHack: The Language that Fixes PHP

7 Aug

We also discuss gradual typing, language design, reactive programming, and AI. 🎙️ https://twp.ai/9OZqsb 2/2

Type Theory Forall reposted

BOB Konferenz

@bobkonf.de

19 June

Video of Julia Himmel's #BOBkonf2026 talk "Proofs for programs, programs for proofs" is now up on our website! bobkonf.de/2026/himmel....

media.ccc.deProofs for programs, programs for proofsProofs about programs are great, but what happens if we let programs and proofs interact in both directions? Lean is both a programming l...

15 June

New Type Theory Forall episode is out! I had the pleasure to partner with @serokell to bring you a conversation with Vladislav Zavialov, one of the main GHC contributors, former GHC Steering Committee member, and current implementer of Dependent Haskell. 1/3

twp.aiyoutu.be#62 - Dependent Haskell - Vladislav Zavialov

15 June

We talked about how GHC is developed, how the Haskell community decides to evolve the language, what it takes to start hacking on GHC, and then went deep into the theory and implementation of Dependent Haskell. This one gets technical in the best way. Watch here: https://twp.ai/4hsWdw 2/3

twp.aiSupport Type Theory Forall • PatreonJoin our Patreon to support the podcast and community. Get behind‑the‑scenes content, early access, and members‑only perks.

15 June

If you enjoy the show, consider supporting TTFA on Patreon, with a one-off donation, or by sponsoring an episode. https://twp.ai/9OXlq0 3/3

2 June

We have an opening in the Type Theory Forall schedule this month for a sponsored episode. 1/3

twp.aiko-fi.comType Theory Forall's Commissions are Open!

2 June

If you'd like to promote your company, research project, open-source tool, conference, or community to an audience interested in programming languages, formal methods, theorem proving, and functional programming, you can commission an episode here: https://twp.ai/9OXQgJ 2/3

lists.seas.upenn.edu [TYPES/announce] Postdoc position in type theory

2 June

Past sponsors have included companies, research groups, conferences, and open-source projects. Feel free to reach out if you have any questions. And if you know someone who might be interested, a retweet would be greatly appreciated for reach. 3/3

Type Theory Forall reposted

Jean Abou Samra

@jeanas.bsky.social

22 May

The Budapest type theory group is hiring a postdoc to work on higher observational type theory. lists.seas.upenn.edu/pipermail/ty...

1 May

The TTFA store is closing May 19. Last chance (for a while) to grab: PL mugs, shirts, hoodies, hats — plus the Tony Hoare tribute drop. https://twp.ai/9OUsKk After a year, we basically broke even — so going forward: • Open once a year • Next reopening: holidays Don’t miss this window.

30 Apr

The TTFA store is closing May 19. Last chance (for a while) to grab: PL mugs, shirts, hoodies, hats — plus the Tony Hoare tribute drop. https://twp.ai/9OUvqF After a year, we basically broke even — so going forward: • Open once a year • Next reopening: holidays Don’t miss this window.

19 Apr

Dropping 2 new items today in tribute to Tony Hoare: • C.A.R T-Shirt • Hoare Triple Hat A small way to celebrate someone who shaped how we think about programming and correctness. https://twp.ai/9OVSQV The store will now only open once a month ⏳ This drop closes May 19 1/2

19 Apr

Then we reopen only for the holidays If you’ve been thinking about getting something — now’s the time. Appreciate all the support ❤️ 2/2

twp.aiType Theory ForallType Theory much beyond inference rules

16 Apr

New TTFA episode I sat down with Farhad Mehta, one of the main organizers of Zurihac, the largest Haskell event in the world. We talk about: • the story behind Zurihac • what it takes to run it • Farhad’s path across academia and industry Zurihac 2026: June 6–8 in Zurich

15 Apr

Cyrus Omar on sabbatical in Cambridge

15 Apr

The store will now only open once a month ⏳ This drop closes May 19 Then we reopen only for the holidays If you’ve been thinking about getting something — now’s the time. Appreciate all the support ❤️ 2/2

Type Theory Forall reposted

@neurocy.bsky.social

10 Apr

Ordered Agda and OCaml mugs from the @ttforall.bsky.social merch store and Pedro threw in a little bonus! 💚

Type Theory Forall reposted

aron

@adler.dev

men are from Type, women are from Prop

Amos Wenger@fasterthanli.me

gf with pred/succ pronouns

Hey everyone! I’ve just started a short series for Patreons where I study and discuss the story of the logicians that make up the intuitionistic lineage. I'm trying to connect the people, ideas, and historical context in a more linear narrative. 1/4

View full thread

I confess that this is not a super well polished video, but if you like foundational papers discussion, I think you'll enjoy this. To share this with a slightly broader audience, I’m offering 50% off the first month on Patreon. 3/4

twp.aiwww.patreon.comPatreon

You can get access to the video through the System F tier for $5 using the discount code DFC5C. https://twp.ai/9PcpYA 4/4

The first episode is out now, and it’s on Frege, centered around his essay “The Thought: A Logical Inquiry.” I think it's a fascinating entry point into how these foundational ideas started to take shape. 2/4

twp.aiwww.youtube.com#60 - Conversations on Life, AI, and the PL Job Market - Pedro and Dan

25 Mar

New TTFA episode 🎙️ What does it mean to build a research career today? With Dan Plyukhin we talk about: • meditation & staying sane • the reality of the job market • reaching out to professors • AI (hype vs reality) • research paths

24 Mar

“The thought, in itself immaterial, clothes itself in the material garment of a sentence and thereby becomes comprehensible to us” — Frege 1956

twp.aitristan.stTristan Stérin

18 Mar

Tristan Stérin used LLMs to hunt for bugs and inconsistencies in Rocq and Lean. This is actually pretty neat and kind of wild.

Today we honor the life and work of Sir Tony Hoare (1934–2026), one of the giants of computer science. His work shaped algorithms, programming languages, concurrency, and formal verification. 1/7

View full thread

Hoare also introduced null references in ALGOL W, which he later called his “billion-dollar mistake,” a candid reflection that pushed language designers toward safer type systems. For these and many other contributions he received the ACM Turing Award in 1980. 6/7

Few researchers have shaped the intellectual foundations of our field so deeply. Thank you, Tony Hoare. May you rest in peace. 7/7

Today we honor the life and work of Sir Tony Hoare (1934–2026), one of the giants of computer science. His work shaped algorithms, programming languages, concurrency, and formal verification. 1/7

View full thread

In 1969 he introduced Hoare Logic in An Axiomatic Basis for Computer Programming, giving us the famous Hoare triple {P} C {Q} and launching the field of formal reasoning about programs. 4/7

He also created Communicating Sequential Processes (CSP), a foundational model for concurrency and message-passing systems that influenced languages and systems for decades. 5/7

Today we honor the life and work of Sir Tony Hoare (1934–2026), one of the giants of computer science. His work shaped algorithms, programming languages, concurrency, and formal verification. 1/7

In 1960, while a visiting student at Moscow State University working on a machine translation project, Hoare needed a way to sort the words of Russian sentences before looking them up in a Russian–English dictionary. 2/7