Informatics Report Series


Report   

EDI-INF-RR-0742


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:A logical framework with dependently typed records
Authors: Thierry Coquand ; Robert Pollack ; Makoto Takeyama
Date:Jan 2005
Publication Title:Fundamenta Informaticae
Publisher:IOS Press
Publication Type:Journal Article Publication Status:Published
Volume No:65(1-2) Page Nos:113-134
ISBN/ISSN:01692968
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh