Internally Typed Second-Order Term Graphs

We present a typing concept for second-order term graphsthat doesnot consider the types as an external add-on, but as an integral part of the term graph structure. This allows a homogeneous treatment of term-graph representations of many kinds of typing systems, including second-order λ-calculi and systems of dependent types. Applications can be found in interactive systems and as typed intermediate representation for example in compilers.