What Sequent Calculus Teaches Us About Computation
9 Jul 2025
A clear breakdown of how λμμ˜-calculus relates to sequent calculus, typing rules, and operational semantics like label/goto.
What Codata, Control Flow, and Logic Teach Us About Programming
9 Jul 2025
Learn how programming concepts like logic, control flow, and evaluation strategy shape the languages we use.
Sequent Calculus vs CPS: A Compiler’s Perspective on Consumers and Evaluation Strategies
9 Jul 2025
Explore how sequent calculus handles consumers, evaluation orders, and eta laws better than CPS, with insights on linear logic and functional compilers.
Why Compiler Writers Care About Case-of-Case
9 Jul 2025
Explore the duality between let-bindings and control operators, and how λμμ˜ calculus enables powerful compiler optimizations like case-of-case.
What Functional Programmers Can Learn from Sequent Calculus
8 Jul 2025
Explore 5 powerful insights into the 𝜆𝜇𝜇˜-calculus, from first-class evaluation contexts to the elegant duality between data and codata types.
How Typing Rules and Type Soundness Work in Core and Fun Programming Languages
8 Jul 2025
Learn how typing rules and type soundness theorems ensure safe program evaluation in Core and Fun, including codata handling and recursive definitions.
Why Type Soundness Matters in Functional Programming Languages
8 Jul 2025
A breakdown of typing rules in Fun and Core languages, with insights into control flow, type soundness, and data vs codata handling.
How Focusing Resolves Stuck Terms in Core Evaluation
8 Jul 2025
Learn how focusing in Core helps eliminate stuck terms, optimize evaluation, and improve program compilation through static transformations.
An Introduction to Evaluation Contexts in Programming Semantics
6 Jul 2025
Evaluation contexts solve nested expression stalls in functional languages like Fun and Core by enabling precise operational semantics.