SubRec is a proof checker for an extension of Martin-Löf's theory of types with dependent record types and subtyping. It provides, in addition, features not present in the proof assistant ALF, like type family declarations, let and use expressions. A very simple XEmacs interface has also been implemented in order to make the proof edition more comfortable.
There is no separate module language in SubRec since the dependent types allow the normal expression language to be used at the module level as well.
The design of SubRec has been heavily influenced by ALF and it was developed while the implementor was a member of the programming logic group at Chalmers, Gothenburg.