Lightnews — Scholar-powered news

Type Theory Forall

@ttforall.bsky.social

110 followers 180 following 100 posts

Making Type Theory, Programming Languages and Formal methods more accessible! http://typetheoryforall.com

typetheoryforall.com

Posts Media Videos Starter Packs

Pinned

Type Theory Forall @ttforall.bsky.social · May 23

🚨 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 @ttforall.bsky.social · 11h

I'm not sure how to implement the solution without typeclasses though, but I think it should be doable

Type Theory Forall @ttforall.bsky.social · 11h

Datatypes à la Carte: www.cambridge.org/core/service...

www.cambridge.org

1 1

Reposted by Type Theory Forall

sabine 🐫🦀 / "use ocaml"; @sabine.sh · 4d

true friendship 🥹

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.

5 18

Reposted by Type Theory Forall

Jonathan Aldrich @jonathanaldrich.bsky.social · 5d

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.

1 3 7

Reposted by Type Theory Forall

One Happy Fellow @onehappyfellow.bsky.social · 9d

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

1 4

Reposted by Type Theory Forall

★ @lexa.qexat.com · 10d

ur type so fat it requires large elimination

3 4 15

Type Theory Forall @ttforall.bsky.social · 9d

That's a good one. I love it! 😂

Type Theory Forall @ttforall.bsky.social · 19d

Schedule a free initial session: calendar.app.google/...

Or email us at [email protected]
5/5

Type Theory Forall @ttforall.bsky.social · 19d

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

Type Theory Forall @ttforall.bsky.social · 19d

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

Type Theory Forall @ttforall.bsky.social · 19d

At Type Theory Forall, we offer 1:1 mentorship in:
• Rocq
• Haskell
• OCaml
• Compilers
• Logic, Abstract Algebra, OO and FP fundaments

We also support students worldwide in preparing strong graduate school applications.
2/5

1 1 2

Type Theory Forall @ttforall.bsky.social · 19d

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

1 1 1

Type Theory Forall @ttforall.bsky.social · 19d

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

store.typetheoryfora...

Type Theory Forall @ttforall.bsky.social · 26d

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

Type Theory Forall @ttforall.bsky.social · Sep 5

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

Type Theory Forall @ttforall.bsky.social · Aug 29

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

Type Theory Forall @ttforall.bsky.social · Aug 27

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

#53 - RustBelt, Iris, and the Art of Writing - Derek Dreyer

Derek Dreyer is a professor at the Max Planck Institute, in 2024 he was awarded the ACM Fellowship, in 2017 he got the ACM Sigplan Robin Milner Young Researcher Award. And has participated or lead greatly influential work, such as the RustBelt Project and Iris. In this episode Derek shares his expe

youtu.be

Type Theory Forall @ttforall.bsky.social · Aug 26

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

Type Theory Forall @ttforall.bsky.social · Aug 26

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

Computability, Philip Wadler

A brief introduction to the hilarious subject of computability theory. Performed as part of Bright Club at The Stand in Edinburgh, on Tuesday 28 April 2015.

www.youtube.com

Type Theory Forall @ttforall.bsky.social · Aug 25

"...somewhat rude." — David Graeber, Are You in a BS Job? In Academe, You're Hardly Alone

Type Theory Forall @ttforall.bsky.social · Aug 25

...It's gotten to the point where "admin" now takes up so much of most professors' time that complaining about it is the default mode of socializing among academic colleagues; indeed, insisting on talking instead about one's latest research project or course idea is considered...

Type Theory Forall @ttforall.bsky.social · Aug 25

"...they study, teach, and write about things ... .

Type Theory Forall @ttforall.bsky.social · Aug 25

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

Type Theory Forall @ttforall.bsky.social · Aug 24

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

Type Theory Forall @ttforall.bsky.social · Aug 23

"How to Present a Paper" by Leslie Lamport, 1979

lamport.azurewebsite...

1 1