Record Calculi. John C. Mitchell, Atsushi Ohori

Roman Cheplyaka pointed me to a good book (Foundations for Programming Languages) by John C. Mitchell. As a side effect, my eye was caught by the author's mention of object-oriented language foundations and record calculi. Record calculi? Really? A few more googles, yes indeed, there are ways to mathematically formalize operations on labeled records, providing for object-oriented languages what lambda calculus provides for functional. First hit on Google Scholar is a 1995 paper by Atsushi Ohori, "Polymorphic record calculus and its compilation"; Ohori in fact has plenty of interesting and publicly available papers. Apparently one use case of this lore is polymorphic type inference for record types in the ML family.