Investigate graphs-as-proofs

[joshsh]

The Curry-Howard-Lambek correspondence is likely to have some important consequences for a graph data model based on lambda calculus. Specifically, an interpretation of types as propositions is likely to suggest a natural framework for knowledge representation and reasoning using λG and Hydra. This might require introducing dependent types. It would be worthwhile to try building up such a framework from first principles, then align it with more conventional frameworks like OWL, and also apply it to property graphs and TinkerPop.

[joshsh]

With respect to dependent types, @wisnesky pointed out the following "dependent types for dummies" recipe: https://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/, which in turn points to this tutorial: https://www.andres-loeh.de/LambdaPi/