#Type-Theory
2 posts in tag “Type-Theory”.
The Curry-Howard Correspondence: How Type Theory Bridges Proof and Computation
2025-03-18Explore 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.
Homotopy Type Theory: The Univalence Axiom, Higher Inductive Types, and ∞-Groupoids
2021-08-11A deep dive into the univalent foundations of mathematics, where equality is homotopy, types are spaces, and the universe mirrors the ∞-groupoid of all ∞-groupoids.