Type Theoretical Databases

4 years 3 months ago
Type Theoretical Databases
Abstract. We present a soundness theorem for a dependent type theory with context conith respect to an indexed category of (finite, abstract) simplical complexes. The point of interest for computer science is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries.
Henrik Forssell, Håkon Robbestad Gylterud, D
Added 07 Apr 2016
Updated 07 Apr 2016
Type Journal
Year 2016
Where LFCS
Authors Henrik Forssell, Håkon Robbestad Gylterud, David I. Spivak
Comments (0)