A Logical Framework with Dependently Typed Records
Thierry Coquand, Randy Beth Pollack, Makoto Takeyama · 2004
this paper we propose an extension of Martin-Lof's logical framework [23, 19] with dependently typed records, and present the semantic fou;7 tion and the typechecking algorithm of ou r system. Some of the work is formally checked in Coq [7]