Programming-Languages

• The Curry-Howard Correspondence: How Type Theory Bridges Proof and Computation · 2025-03-18

  Explore the profound isomorphism between logical proofs and computer programs: how the Curry-Howard correspondence unifies propositional logic with typed lambda calculus, and how it enables modern proof assistants like Coq, Lean, and Agda.

• Compiler Optimizations: From Source Code to Fast Machine Code · 2020-09-23

  A deep dive into how modern compilers transform your code into efficient machine code. Explore optimization passes from constant folding to loop vectorization, and learn how to write code that compilers can optimize effectively.