Towards a Formalisation of Relational Database Theory in Constructive Type Theory

Carlos Gonzalia

doi:10.1007/978-3-540-24771-5_12

Towards a Formalisation of Relational Database Theory in Constructive Type Theory

Carlos Gonzalia

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

5 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 language	English
Title of host publication	Relational and Kleene-Algebraic Methods in Computer Science
Editors	R. Berghammer, B. Maller, G. Struth
Place of Publication	Berlin ; Heidelberg, Germany
Publisher	Springer, Springer Nature
Pages	137-148
Number of pages	12
Volume	3051
ISBN (Print)	9783540221456
DOIs	https://doi.org/10.1007/978-3-540-24771-5_12
Publication status	Published - 2004
Externally published	Yes
Event	7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra - Bad Malente, Germany Duration: 12 May 2003 → 17 May 2003

Workshop

Workshop	7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra
City	Bad Malente, Germany
Period	12/05/03 → 17/05/03

Keywords

type theory
relational database model
computer formalization of proofs
logical frameworks

Access to Document

10.1007/978-3-540-24771-5_12

Cite this

@inproceedings{4bb11327adb94ce0b3e3566c9d0b2629,

title = "Towards a Formalisation of Relational Database Theory in Constructive Type Theory",

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{\"o}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.",

keywords = "type theory, relational database model, computer formalization of proofs, logical frameworks",

author = "Carlos Gonzalia",

year = "2004",

doi = "10.1007/978-3-540-24771-5_12",

language = "English",

isbn = "9783540221456",

volume = "3051",

pages = "137--148",

editor = "R. Berghammer and B. Maller and G. Struth",

booktitle = "Relational and Kleene-Algebraic Methods in Computer Science",

publisher = "Springer, Springer Nature",

address = "United States",

note = "7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra ; Conference date: 12-05-2003 Through 17-05-2003",

}

Gonzalia, C 2004, Towards a Formalisation of Relational Database Theory in Constructive Type Theory. in R Berghammer, B Maller & G Struth (eds), Relational and Kleene-Algebraic Methods in Computer Science. vol. 3051, Springer, Springer Nature, Berlin ; Heidelberg, Germany, pp. 137-148, 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra, Bad Malente, Germany, 12/05/03. https://doi.org/10.1007/978-3-540-24771-5_12

Towards a Formalisation of Relational Database Theory in Constructive Type Theory. / Gonzalia, Carlos.
Relational and Kleene-Algebraic Methods in Computer Science. ed. / R. Berghammer; B. Maller; G. Struth. Vol. 3051 Berlin ; Heidelberg, Germany: Springer, Springer Nature, 2004. p. 137-148.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding contribution › peer-review

TY - GEN

T1 - Towards a Formalisation of Relational Database Theory in Constructive Type Theory

AU - Gonzalia, Carlos

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

KW - type theory

KW - relational database model

KW - computer formalization of proofs

KW - logical frameworks

U2 - 10.1007/978-3-540-24771-5_12

DO - 10.1007/978-3-540-24771-5_12

M3 - Conference proceeding contribution

SN - 9783540221456

VL - 3051

SP - 137

EP - 148

BT - Relational and Kleene-Algebraic Methods in Computer Science

A2 - Berghammer, R.

A2 - Maller, B.

A2 - Struth, G.

PB - Springer, Springer Nature

CY - Berlin ; Heidelberg, Germany

T2 - 7th International Seminar on Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra

Y2 - 12 May 2003 through 17 May 2003

ER -