The project is motivated by two observations: (i) there is currently a shift from relational to Graph Databases (GDBs) that still suffer from a lack of a formal semantics; (ii) GDBs not only have to be queried, but also transformed in a meaningful and reliable way. The project will address these issues by making decisive contributions at the interface of GDBs and Programming Language Theory, by (1) enriching GDBs with formal semantic information; (2) verifying and informing the design of the next generation of graph query languages; (3) defining graph transformation and schema mapping languages with a formal semantics to permit fully automated verification of enforcement of consistency constraints. The project will have a considerable impact on the formal semantics of a new ISO Standard for a GDB query language, along with property graph transformations for data integration and data curation.