Type Theoretical Databases

DOI10.1007/978-3-319-27683-0_9zbMATH Open1474.68099arXiv1406.6268OpenAlexW2963574586MaRDI QIDQ5283422FDOQ5283422

Håkon Robbestad Gylterud, Henrik Forssell, David I. Spivak

Publication date: 21 July 2017

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Abstract: We present a soundness theorem for a dependent type theory with context constants with 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.

Full work available at URL: https://arxiv.org/abs/1406.6268

zbMATH Keywords

relational databasesdependent type theorysimplicial sets

Mathematics Subject Classification ID

Database theory (68P15) Simplicial sets, simplicial objects (18N50) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Categorical logic and type theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Survey article: an elementary illustrated introduction to simplicial sets
• Title not available (Why is that?)
• Type Theoretical Databases

Cited In (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Relational and Kleene-Algebraic Methods in Computer Science
• Type Theoretical Databases

This page was built for publication: Type Theoretical Databases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5283422)