dep. record types?

[This will be the first of several types postings during the next few
minutes -- I've just returned to the electronic world after a break
for POPL.  --BCP]


I stumbled across the definition of DEPENDENT
RECORD TYPES due to G. Betarte and A. Tasistro
(in "Extension of Martin-Lof's theory of types
with record types and subtyping:
motivation, rules and type checking"),
and I would like to know more about the notion 
of record types is general. I have two questions:

- Is the definition of Betarte&Tasistro
for dependent record types *THE* definition,
or is the name (dependent) record type being
used for many more (different) notions?

-Does anybody know any relevant references
on this matter (record types, dependent record 
types, sigma types etc)?

Thanking in advance,
Mirna Bognar