Mathematics

• Linear Logic: Girard's Resource-Sensitive Logic, Exponential Modalities, and Linear Types in Rust · 2021-09-29

  A comprehensive exploration of linear logic's resource-conscious foundations, proof nets, the ! and ? modalities translating intuitionistic to linear, and how Rust's ownership system mirrors these ideas.

• Homotopy Type Theory: The Univalence Axiom, Higher Inductive Types, and ∞-Groupoids · 2021-08-11

  A deep dive into the univalent foundations of mathematics, where equality is homotopy, types are spaces, and the universe mirrors the ∞-groupoid of all ∞-groupoids.

• Category Theory for Programmers: Functors, Monads, and Natural Transformations · 2021-08-10

  A rigorous yet intuitive journey through the categorical structures that secretly power functional programming—from categories and functors to adjunctions and the monad-as-monoid correspondence.