Rust
- 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.
- Region-Based Memory Management: Tofte & Talpin's Region Inference, the ML Kit, Safety Proofs, and the Relationship to Rust's Lifetimes
· 2020-12-01
A 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.