Skip to main content
SpringerLink
Log in

Type Theoretical Databases

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9537))

Included in the following conference series:

Abstract

We show how the display-map category of finite simplicial complexes can be seen as representing the totality of database schemas and instances in a single mathematical structure. We give a sound interpretation of a certain dependent type theory in this model, and show how it allows for the syntactic specification of schemas and instances and the manipulation of the same with the usual type-theoretic operations. We indicate how it allows for the posing of queries. A novelty of the type theory is that it has non-trivial context constants.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Coming from reasons having to do with simplicity and wanting to stay close to the view of tables as relations, this requirement, and indeed the structure of the schemas we are considering, does mean that a certain care has to be taken with attribute names at the modeling level. For instance whether one should, when faced with two tables with exactly the same attributes, collect these into one table (possibly with an extra column), rename some attributes, or introduce new “dummy” or “relation name” attributes to keep the two tables apart. For reasons of space, we do not discuss these issues here.

  2. 2.

    Strictly speaking, we choose an isomorphic representation which is strict and stable under substitution. For current purposes, however, the current definition is notationally convenient.

References

  1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)

    MATH  Google Scholar 

  2. Cartmell, J.: Formalising the network and hierarchical data models — an application of categorical logic. In: Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 466–492. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  3. Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  4. Forssell, H., Gylterud, H.R., Spivak, D.I.: Type theoretical databases (2014). http://arxiv.org/abs/1406.6268

  5. Friedman, G.: Survey article: an elementary illustrated introduction to simplicial sets. Rocky Mt. J. Math. 42(2), 353–423 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  6. Gabriel, P., Zisman, M.: Calculus of Fractions and Homotopy Theory. Springer, Heidelberg (1967)

    Book  MATH  Google Scholar 

  7. Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)

    MATH  Google Scholar 

  8. Mac Lane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  9. Martin-Löf, P.: Intuitionistic Type Theory. Studies in Proof Theory, vol. 1. Bibliopolis, Naples (1984)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, University of Oslo, Oslo, Norway

    Henrik Forssell

  2. Department of Mathematics, Stockholm University, Stockholm, Sweden

    Håkon Robbestad Gylterud

  3. Department of Mathematics, MIT, Cambridge, MA, USA

    David I. Spivak

Authors
  1. Henrik Forssell
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Håkon Robbestad Gylterud
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David I. Spivak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Håkon Robbestad Gylterud .

Editor information

Editors and Affiliations

  1. City University of New York , New York, New York, USA

    Sergei Artemov

  2. Cornell University , Ithaca, New York, USA

    Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Forssell, H., Gylterud, H.R., Spivak, D.I. (2016). Type Theoretical Databases. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2016. Lecture Notes in Computer Science(), vol 9537. Springer, Cham. https://doi.org/10.1007/978-3-319-27683-0_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27683-0_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27682-3

  • Online ISBN: 978-3-319-27683-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation