Towards a Formalisation of Relational Database Theory in Constructive Type Theory

Carlos Gonzalia

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

3 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationRelational and Kleene-Algebraic Methods in Computer Science
EditorsR. Berghammer, B. Maller, G. Struth
Place of PublicationBerlin ; Heidelberg, Germany
PublisherSpringer, Springer Nature
Pages137-148
Number of pages12
Volume3051
ISBN (Print)9783540221456
DOIs
Publication statusPublished - 2004
Externally publishedYes
Event7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra - Bad Malente, Germany
Duration: 12 May 200317 May 2003

Workshop

Workshop7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra
CityBad Malente, Germany
Period12/05/0317/05/03

Keywords

  • type theory
  • relational database model
  • computer formalization of proofs
  • logical frameworks

Fingerprint Dive into the research topics of 'Towards a Formalisation of Relational Database Theory in Constructive Type Theory'. Together they form a unique fingerprint.

Cite this