Programming-Languages
2 posts in category “Programming-Languages”.
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.
Region-Based Memory Management: Tofte & Talpin's Region Inference, the ML Kit, Safety Proofs, and the Relationship to Rust's Lifetimes
2020-12-01A deep exploration of region-based memory management — how Tofte and Talpin's region inference eliminates garbage collection while preserving memory safety, and how their ideas echo through Rust's ownership and borrowing system.