Type theoretical databases

DOI10.1007/978-3-319-27683-0_9MaRDI QIDQ5283422zbMATH OpenOpenAlexFDO

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

Publication date 21 July 2017

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

Full work available at URL https://arxiv.org/abs/1406.6268, http://hdl.handle.net/10852/85289

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)

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.

Recommendations

• Type theoretical databases
• Algebraic databases
• Functorial data migration
• scientific article; zbMATH DE number 1522507
• Publication:4490753

Cites work

• scientific article; zbMATH DE number 4014080 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 839556 (Why is no real title available?)
• scientific article; zbMATH DE number 3297895 (Why is no real title available?)
• Categorical logic and type theory
• Survey article: an elementary illustrated introduction to simplicial sets
• Type theoretical databases

Cited in

(8)

• Functorial data migration
• scientific article; zbMATH DE number 1696786 (Why is no real title available?)
• Zeta types and Tannakian symbols as a method for representing mathematical knowledge
• scientific article; zbMATH DE number 3999265 (Why is no real title available?)
• Institutions for SQL database schemas and datasets
• Type theoretical databases
• Type theoretical databases
• Relational and Kleene-Algebraic Methods in Computer Science

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)