We show how the display-map category of finite simplicial complexes can be seen as representing the totality of database schemas and instances in a single mathematical structure. We give a sound interpretation of a certain dependent type theory in this model, and show how it allows for the syntactic specification of schemas and instances and the manipulation of the same with the usual type-theoretic operations. We indicate how it allows for the posing of queries. A novelty of the type theory is that it has non-trivial context constants.
CITATION STYLE
Forssell, H., Gylterud, H. R., & Spivak, D. I. (2016). Type theoretical databases. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9537, pp. 117–129). Springer Verlag. https://doi.org/10.1007/978-3-319-27683-0_9
Mendeley helps you to discover research relevant for your work.