Towards a Formalisation of Relational Database Theory in Constructive Type Theory

  • Carlos Gonzalía
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)


We offer here an overview of several initial attempts of formalisation of relational database theory in a constructive, type-theoretic, framework. Each successive formalisation is of more generality, and correspondingly more complex, than the previous one. All our work is carried out in the proof editor Alfa for Martin-Löf’s monomorphic type theory. Our goal is to obtain a formalisation that provides us with computational content, instead of just being a completely abstract theory.


Relational Database Type Theory Logical Constant Database Operation Collection Operation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Augustsson, L.: Cayenne - a language with dependent types. In: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, 1998, Baltimore, Maryland, United States, pp. 239–250. ACM Press, New York (1998)Google Scholar
  2. 2.
    Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. Journal of Functional Programming 13(2), 261–293 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Codd, E.F.: A Relational Model of Data for Large Shared Data Banks. Communications of the ACM 13(6), 377–387 (1970)zbMATHCrossRefGoogle Scholar
  4. 4.
    Coquand, C.: Agda home page,
  5. 5.
    Coquand, C., Coquand, T.: Structured Type Theory. In: Proceedings of Part of PLI 1999 (Colloquium on Principles, Logics, and Implementations of High- Level Programming Languages). Workshop on Logical Frameworks and Meta-languages, Paris, France (September 1999)Google Scholar
  6. 6.
    Darwen, H., Date, C.J.: The Third Manifesto. ACM SIGMOD Record 24(1), 39–49 (1995)CrossRefGoogle Scholar
  7. 7.
    Gonzalía, C.: The Allegory of E-Relations in Constructive Type Theory. In: Desharnais, J., Frappier, M., MacCaull, W. (eds.) Relational Methods in Computer Science: The Québec Seminar, April 2002, pp. 19–38. Methoδos Verlag (2002)Google Scholar
  8. 8.
    Gonzalía, C.: Relation Calculus in Martin-Löf Type Theory. Ph. Lic. thesis, Technical Report no. 5L, Department of Computing Science, Chalmers University of Technology and Göteborg University (February 2002)Google Scholar
  9. 9.
    Hallgren, T.: Alfa home page,
  10. 10.
    Hedberg, M.: New standard library for Alfa,
  11. 11.
    Kawahara, Y., Okhuma, H.: Relational Aspects of Relational Database Dependencies. In: Desharnais, J. (ed.) RelMICS 2000: 5th International Seminar on Relational Methods in Computer Science, Valcartier, Québec, Canada, January 2000, pp. 185–194 (2000)Google Scholar
  12. 12.
    Mäenpää, P., Tikkanen, M.: Dependent Types in Databases. In: Workshop in Dependent Types in Programming, Göteborg, Sweden (1999)Google Scholar
  13. 13.
    Nordström, B., Petersson, K., Smith, J.: Programming in Martin-Löf ’s Type Theory. An Introduction. The International Series of Monographs on Computer Science. Oxford University Press, Oxford (1990)zbMATHGoogle Scholar
  14. 14.
    Rajagopalan, P., Tsang, C.P.: A Generic Algebra for Data Collections Based on Constructive Logic. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 546–560. Springer, Heidelberg (1995)Google Scholar
  15. 15.
    Schmidt, G., Ströhlein, T.: Relations and Graphs. Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Carlos Gonzalía
    • 1
  1. 1.Department of Computing ScienceChalmers University of Technology and Gothenburg UniversityGothenburgSweden

Personalised recommendations