Dependent Record Types, Subtyping and Proof Reutilization (2007)
Gustavo Betarte, Gustavo Betarte (draft
. We present an example of formalization of systems of algebras using an extension of Martin-Lof's theory of types with record types and subtyping. This extension has been presented in [5]. In...