2018/10/29 by Hongwei Xi, Xi, Hongwei, Dengping Zhu +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1810.12190
openalex publication_date 2018/10/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present a type system capable of guaranteeing the memory safety of programs that may involve (sophisticated) pointer manipulation such as pointer arithmetic. With its root in a recently developed framework Applied Type System (ATS), the type system imposes a level of abstraction on program states through a novel notion of recursive stateful views and then relies on a form of linear logic to reason about such stateful views. We consider the design and then the formalization of the type system to constitute the primary contribution of the paper. In addition, we also mention a running implementation of the type system and then give some examples in support of the practicality of programming with recursive stateful views.