Constrained Horn Clauses (CHCs) are an intermediate program
representation that can be generated by several verification tools,
and that can be processed and solved by a number of Horn solvers. One
of the main challenges when using CHCs in verification is the encoding
of heap-allocated data-structures: such data-structures are today
either represented explicitly using the theory of arrays, or
transformed away with the help of invariants or refinement types,
defeating the purpose of CHCs as a representation that is
language-independent as well as agnostic of the algorithm implemented
by the Horn solver.  This paper presents an SMT-LIB theory of heaps
tailored to CHCs, with the goal of enabling a standard interchange
format for programs with heap data-structures. We introduce the syntax
of the theory of heaps, define its semantics in terms of axioms and
using a reduction to SMT-LIB arrays and data-types, provide an
experimental evaluation and outline possible extensions and future
work.