CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Towards a Formalisation of Relational Database Theory in Constructive Type Theory

Carlos Gonzalía (Institutionen för data- och informationsteknik, datavetenskap (GU) ; Institutionen för datavetenskap)
Relational and Kleene-Algebraic Methods in Computer Science: 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised Selected Papers Vol. LNCS (2004), 3051, p. 137-148.
[Konferensbidrag, refereegranskat]

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öfrsquos monomorphic type theory. Our goal is to obtain a formalisation that provides us with computational content, instead of just being a completely abstract theory.

Nyckelord: type theory, relational databases, formalized mathematics

Denna post skapades 2006-08-25. Senast ändrad 2013-03-13.
CPL Pubid: 12216


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, datavetenskap (GU) (GU)
Institutionen för datavetenskap (2002-2004)


Teoretisk datalogi

Chalmers infrastruktur