A general framework for types in graph rewriting

We investigate a general framework which can be instantiated in order to obtain type systems for graph rewriting, allowing us to statically infer behavioural properties of a graph. We describe conditions such as the subject reduction property and compositionality that should be satisfied by such a framework. We present a methodology for proving these conditions, specifically we prove that it is sufficient to show properties that are local to graph transformation rules. In order to show the applicability of this framework, we describe in several case studies how to integrate existing type systems (for the π-calculus and the λ-calculus) and a system for typing acyclic graphs. This is a completely revised and extended version of a paper of which an earlier version has appeared in FSTTCS '00.