Core Theory & Foundations

This area focuses on the mathematical underpinnings of computation. Researchers here don't just build languages; they prove properties about them.

Type Theory

The study of type systems (e.g., static vs. dynamic, dependent types, linear types) which serve as a logic to prove that programs behave correctly before they run.

Formal Semantics

Rigorous mathematical specification of the meaning of programs.

• Operational Semantics: How a program is executed (step-by-step).
• Denotational Semantics: What a program computes (mapping to mathematical objects).

Category Theory in PL

Using abstract algebra to model compositional structures in programming (e.g., Monads, Functors).

Lambda Calculus & Combinatory Logic

Studying the smallest possible models of computation that underpin functional languages.