Henrik Forssell and Håkon R. Gylterud: Type theoretical databases

We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. From a computer science perspective, the interesting point 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. This is joint work with David I. Spivak (MIT).