Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Type Theoretical Databases
Stockholm University, Faculty of Science, Department of Mathematics.
Stockholm University, Faculty of Science, Department of Mathematics.
Massachusetts Institute of Technology, USA.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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.

Keyword [en]
database, type theory, universe, schema, simplicial complex
National Category
Algebra and Logic Computer and Information Science
Research subject
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-136895OAI: oai:DiVA.org:su-136895DiVA: diva2:1057510
Available from: 2016-12-18 Created: 2016-12-18 Last updated: 2016-12-22Bibliographically approved
In thesis
1. Univalent Types, Sets and Multisets: Investigations in dependent type theory
Open this publication in new window or tab >>Univalent Types, Sets and Multisets: Investigations in dependent type theory
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

Place, publisher, year, edition, pages
Stockholm: Department of Mathematics, Stockholm University, 2017. 173 p.
Keyword
type theory, homotopy type theory, dependent types, constructive set theory, databases, formalisation, agda
National Category
Mathematics
Research subject
Mathematics
Identifiers
urn:nbn:se:su:diva-136896 (URN)978-91-7649-654-1 (ISBN)978-91-7649-655-8 (ISBN)
Public defence
2017-02-09, sal 14, hus 5, Kräftriket, Roslagsvägen 101, Stockholm, 13:00 (English)
Opponent
Supervisors
Available from: 2017-01-17 Created: 2016-12-18 Last updated: 2017-01-17Bibliographically approved

Open Access in DiVA

No full text

Other links

arXiv:1406.6268

Search in DiVA

By author/editor
Forssell, HenrikRobbestad Gylterud, Håkon
By organisation
Department of Mathematics
Algebra and LogicComputer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Total: 14 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf