Type theory with records

Type theory with records is a formal semantics representation framework, using "records" to express type theory "types". It has been used in natural language processing, principally computational semantics and dialogue systems.
Syntax.
A "record type" is a set of fields. A field is a pair consisting of a label and a type. Within a record type, field labels are unique. The witness of a record type is a "record". A record is a similar set of fields, but fields contain objects instead of types. The object in each field must be of the type declared in the corresponding field in the record type.
Basic type: formula_1
Object: formula_2
Ptype: formula_3
Object: formula_4
where formula_5 and formula_6 are individuals (type formula_7), formula_8 is proof that formula_5 is a boy, etc.