A Logical Framework with Dependently Typed Records

Abstract

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]