A type system for safe memory management and its proof of correctness | Publicación