{'fraction_non_alphanumeric': 0.015130674002751032, 'fraction_numerical': 0.0, 'mean_word_length': 4.824, '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}}
A Deep Embedding of a Decidable Fragment of Separation Logic in HOL

Smallfoot is a tool to automatically check separation logic specifications of sequential programs. It uses a decidable fragment of separation logic. In this paper, a deep embedding of a slightly different decidable fragment of separation logic inspired by Smallfoot is presented. Moreover, a HOL implementation of a decision procedure for entailments in this logic is described. The main focus of this paper is on the introduction of the separation logic at an high level of abstraction and on inference rules for entailments. It is pointed out how these high-level concepts relate to the HOL embedding. However, the HOL embedding is not explained in detail.