- Abstract:
-
Our long term goal is a system to formally represent complex structured mathematical objects, and proofs and computation on such objects; e.g.\ a foundational computer algebra system. Our approach is informed by the long development of module systems for functional programming based on dependent record types as signatures. For our logical purposes, however, we want a dependently typed base language. In this paper we propose an extension of Martin-L\"of's logical framework with dependently typed records, and present the semantic foundation and the typechecking algorithm of our system.
- Links To Paper
- No links available
- Bibtex format
- @Article{EDI-INF-RR-0742,
- author = {
Thierry Coquand
and Robert Pollack
and Makoto Takeyama
},
- title = {A logical framework with dependently typed records},
- journal = {Fundamenta Informaticae},
- publisher = {IOS Press},
- year = 2005,
- month = {Jan},
- volume = {65(1-2)},
- pages = {113-134},
- }
|