[Prev][Next][Index][Thread]
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]
Hello!
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