{'fraction_non_alphanumeric': 0.014214046822742474, 'fraction_numerical': 0.0, 'mean_word_length': 5.613259668508287, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Extended alias type system using separating implication

Although explicit memory management is necessary to implement low-level software such as operating systems and language runtime systems, it is prohibited by conventional strictly typed programming languages because it violates the type preservation of memory regions, a property that ensures the type safety of programs. The alias type system allows explicit memory management without the loss of type safety by statically tracking pointers and their aliases. However, it suffers from limitations in handling recursive data structures because it requires complete information about the pointer aliases. In this paper, we propose an extension of the alias type system using separating implications, which are derived from separation logic. Separating implications enable us to handle recursive data structures with incomplete aliasing information by assuming aliasing relations in a part of memory. The proposed type system is capable of expressing tail-recursive operations on recursive data structures. For example, we can implement a FIFO queue with constant-time operations; this cannot be achieved using the original alias type system.