28.02.2026 18:30 —
👍 1
🔁 0
💬 0
📌 0
28.02.2026 18:30 —
👍 1
🔁 0
💬 0
📌 0
For students and engineers working in PL, compilers, or formal verification, understanding these three perspectives is essential. They are not competing views. They are complementary lenses on what programs are and what it means for them to be correct.
8/8
This tradition gave us foundational ideas such as invariants and Hoare logic, emphasizing reasoning as central to programming.
Operational semantics models execution.
Denotational semantics models mathematical meaning.
Axiomatic semantics models provability.
7/8
Axiomatic semantics shifts the focus from behavior to provable properties. Rather than defining execution and then deriving laws, it takes logical rules as primary. The meaning of a program is given by what can be proven about it.
6/8
This perspective enables equational reasoning, compositionality, and deep connections with domain theory.
Denotational semantics answers the question: what mathematical object does this program denote?
3) Axiomatic semantics
5/8
Denotational semantics abstracts away from execution and maps programs directly to mathematical objects such as numbers, functions, or more structured semantic domains.
Instead of describing steps of evaluation, we define an interpretation function from syntax to a semantic domain.
4/8
Different operational presentations can model different levels of abstraction, and proving their correspondence amounts to proving implementation correctness.
Operational semantics answers the question: how does this program run?
2) Denotational semantics
3/8
A machine state is typically just a term of the language, and evaluation proceeds by transitions between states.
In small step semantics, execution is modeled as a sequence of reduction steps. In big step semantics, evaluation relates a term directly to its final value.
2/8
Once we formalize the syntax of a language, the next step is to formalize its semantics: what programs mean and how they behave.
There are three classical approaches.
1) Operational semantics
Operational semantics defines meaning by describing how programs execute on an abstract machine.
1/8
In a few minutes we are going live on Twitch to watch and discuss selected ICFP talks together.
If you are interested in programming languages research, semantics, type systems, and formal methods, join us for a live session of collective viewing and commentary.
going to do some #LeanLang streaming for the first time in a while!
i tried to get claude code to add polymorphism to my formalisation of HM. let's see what it managed to do and where it got stuck. join me as i do some forensic analysis 🕵️
starting at 7:30pm UTC today!
www.twitch.tv/aronadler
90+ hours interviewing the best minds in type theory.
Now you can wear (and sip from) the movement.
The Type Theory Forall store is up and running.
Apparel and mugs for people who care about foundations.
Every purchase helps keep deep PL conversations alive.
https://twp.ai/9PbfTY
New semester just started.
If your Rocq file already has 37 unsolved goals
If your compiler project looks… concerning
I’m opening tutoring spots in:
• Rocq
• Haskell / OCaml
• Compilers
• Logic & Algebra
Strong foundations. No shortcuts.
Free intro call 👇
90+ hours interviewing the best minds in type theory.
Now you can wear (and sip from) the movement.
The Type Theory Forall store is up and running.
Apparel and mugs for people who care about foundations.
Every purchase helps keep deep PL conversations alive.
https://twp.ai/9PbTgF
"Readable formal specifications are not a convenience that AI can replace. They are the foundation of trust."
19.02.2026 00:53 — 👍 3 🔁 1 💬 0 📌 0
If you are interested in learning more about type theory, programming languages, and proof assistants, follow us here and subscribe on YouTube www.youtube.com/@typ...
9/9
For students and engineers working on compilers, DSLs, or formal methods, type theory is not an abstract curiosity. It is the language in which we make precise claims about programs and then prove them.
8/9
In an era of AI assisted development, proof assistants offer a different paradigm. Instead of generating plausible text, we iteratively construct machine checked proofs against a formal specification. The result is not just confidence. It is correctness by construction.
7/9
This is not marketing. It is mechanized metatheory.
3) Proof assistants and formal verification
Type theory is the theoretical backbone of systems such as Lean, Rocq, Agda, and Isabelle/HOL. These are programmable logics where specifications and proofs coexist with code.
6/9
2) Industrial impact: Rust and RustBelt
Careful type theoretic design eliminates entire classes of bugs at compile time. The RustBelt project went further and formally verified core aspects of Rust’s type system using the Rocq proof assistant, with peer reviewed results in top PL venues.
5/9
As Dijkstra wrote, “Program testing can be used to show the presence of bugs, but never to show their absence.” Tests explore a finite search space. Proofs quantify over infinite domains. Type theory is the foundation that makes such proofs possible in programming language research.
4/9
1) Programming language design and metatheory
Type theory provides the tools to state and prove properties such as type safety, normalization, and parametricity. These results are not testing heuristics. They are mathematical guarantees.
3/9
It investigates how types enforce invariants, guarantee safety properties, and shape the design of programming languages.
Its impact is both theoretical and practical.
2/9
People often ask: what is type theory and why is it useful?
Type Theory is the academic study of type systems: formal frameworks for classifying terms, structuring computation, and specifying the behavior of programs. 🧵
1/9
Also we have the possibility for commissioned episodes!
If there’s a topic or researcher you’d really like to see featured, you can sponsor an episode here:
ko-fi.com/typetheory...
If you’re unsure whether your idea makes sense, just DM me. I’m always happy to talk it through 🤝
I’m planning next month’s Type Theory Forall episodes and I’d genuinely love your input.
What would you be interested to hear next?
Proof theory?
Modern Programming Language Semantics?
Lean or Rocq?
Compilers?
AI × formal methods?
Is there a paper, idea, or person you think I should talk to?
90+ hours interviewing the best minds in type theory.
Now you can wear (and sip from) the movement.
The Type Theory Forall store is up and running.
Apparel and mugs for people who care about foundations.
Every purchase helps keep deep PL conversations alive.
https://twp.ai/9PbYfP
An ode to the International PhD Student
"To the one living between time zones.
Between ambition and homesickness.
Between gratitude and guilt. "
https://twp.ai/9PbVnL
New semester just started.
If your Rocq file already has 37 unsolved goals
If your compiler project looks… concerning
I’m opening tutoring spots in:
• Rocq
• Haskell / OCaml
• Compilers
• Logic & Algebra
Strong foundations. No shortcuts.
Free intro call 👇
90+ hours interviewing the best minds in type theory.
Now you can wear (and sip from) the movement.
The Type Theory Forall store is up and running.
Apparel and mugs for people who care about foundations.
Every purchase helps keep deep PL conversations alive.
https://twp.ai/9PbYcf