  Graphs are a generalized concept that encompasses more complex data
structures than trees, such as difference lists, doubly-linked lists, skip
lists, and leaf-linked trees. Normally, these structures are handled with
destructive assignments to heaps, which is opposed to a purely functional
programming style and makes verification difficult. We propose a new purely
functional language, $\lambda_{GT}$, that handles graphs as immutable,
first-class data structures with a pattern matching mechanism based on Graph
Transformation and developed a new type system, $F_{GT}$, for the language. Our
approach is in contrast with the analysis of pointer manipulation programs
using separation logic, shape analysis, etc. in that (i) we do not consider
destructive operations but pattern matchings over graphs provided by the new
higher-level language that abstract pointers and heaps away and that (ii) we
pursue what properties can be established automatically using a rather simple
typing framework.
