Towards a聽Formalisation of Relational Database Theory in Constructive Type Theory
| 详细信息 | 推荐本文 | |
- 作者：Carlos Gonzal铆a
- 刊名：Lecture Notes in Computer Science
- 出版时间：2004
- 出版年：2004
- 期刊代码：99_0302-9743
- 类别：cp
- 卷：3051
- 期：1
- 页码：137-148
- 数据来源：sp
摘要
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öfs monomorphic type theory. Our goal is to obtain a formalisation that provides us with computational content, instead of just being a completely abstract theory.